# Subalgebras and directed Unions of sets #

## Main results #

- `Subalgebra.coe_iSup_of_directed`: a directed supremum consists of the union of the algebras
- `Subalgebra.iSupLift`: define an algebra homomorphism on a directed supremum of subalgebras by defining it on each subalgebra, and proving that it agrees on the intersection of subalgebras.

source
theorem Subalgebra.coe_iSup_of_directed {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Type u_4} [Nonempty ι] {K : ι → Subalgebra R A} (dir : Directed (fun (x1 x2 : Subalgebra R A) => x1 ≤ x2) K) :
↑(iSup K) = ⋃ (i : ι), ↑(K i)
source
noncomputable def Subalgebra.iSupLift {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_4} [Nonempty ι] (K : ι → Subalgebra R A) (dir : Directed (fun (x1 x2 : Subalgebra R A) => x1 ≤ x2) K) (f : (i : ι) → ↥(K i) →ₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)) (T : Subalgebra R A) (hT : T = iSup K) :
↥T →ₐ[R] B

Define an algebra homomorphism on a directed supremum of subalgebras by defining it on each subalgebra, and proving that it agrees on the intersection of subalgebras.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Subalgebra.iSupLift_inclusion {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_4} [Nonempty ι] (K : ι → Subalgebra R A) {dir : Directed (fun (x1 x2 : Subalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (h : K i ≤ T) :
(iSupLift K dir f hf T hT) ((inclusion h) x) = (f i) x
source
@[simp]
theorem Subalgebra.iSupLift_comp_inclusion {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_4} [Nonempty ι] (K : ι → Subalgebra R A) {dir : Directed (fun (x1 x2 : Subalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T) :
(iSupLift K dir f hf T hT).comp (inclusion h) = f i
source
@[simp]
theorem Subalgebra.iSupLift_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_4} [Nonempty ι] (K : ι → Subalgebra R A) {dir : Directed (fun (x1 x2 : Subalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (hx : ↑x ∈ T) :
(iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x
source
theorem Subalgebra.iSupLift_of_mem {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Type u_4} [Nonempty ι] (K : ι → Subalgebra R A) {dir : Directed (fun (x1 x2 : Subalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥T) (hx : ↑x ∈ K i) :
(iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩