Subalgebras and directed Unions of sets #
Main results #
Subalgebra.coe_iSup_of_directed: a directed supremum consists of the union of the algebrasSubalgebra.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.
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)
:
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 (Subalgebra.inclusion h))
(T : Subalgebra R A)
(hT : T = iSup K)
:
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
@[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 (Subalgebra.inclusion h)}
{T : Subalgebra R A}
{hT : T = iSup K}
{i : ι}
(x : ↥(K i))
(h : K i ≤ T)
:
(Subalgebra.iSupLift K dir f hf T hT) ((Subalgebra.inclusion h) x) = (f i) x
@[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 (Subalgebra.inclusion h)}
{T : Subalgebra R A}
{hT : T = iSup K}
{i : ι}
(h : K i ≤ T)
:
(Subalgebra.iSupLift K dir f hf T hT).comp (Subalgebra.inclusion h) = f i
@[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 (Subalgebra.inclusion h)}
{T : Subalgebra R A}
{hT : T = iSup K}
{i : ι}
(x : ↥(K i))
(hx : ↑x ∈ T)
:
(Subalgebra.iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x
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 (Subalgebra.inclusion h)}
{T : Subalgebra R A}
{hT : T = iSup K}
{i : ι}
(x : ↥T)
(hx : ↑x ∈ K i)
:
(Subalgebra.iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩