Documentation

Mathlib.Algebra.Algebra.Subalgebra.Directed

Subalgebras and directed Unions of sets #

Main results #

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
theorem Subalgebra.coe_iSup_eq_iUnion_finset_coe_biSup {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Type u_5} (S : ι → Subalgebra R A) :
↑(⨆ (i : ι), S i) = ⋃ (s : Finset ι), ↑(⨆ i ∈ s, S i)
source
theorem Subalgebra.isMulCommutative_iSup {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Type u_4} [Nonempty ι] {S : ι → Subalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)] (dir : Directed (fun (x1 x2 : Subalgebra R A) => x1 ≤ x2) S) :
IsMulCommutative ↥(⨆ (i : ι), S i)
source
instance Subalgebra.instIsMulCommutative_iSup {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Type u_4} [Nonempty ι] [Preorder ι] [IsDirectedOrder ι] {S : ι →o Subalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)] :
IsMulCommutative ↥(⨆ (i : ι), S 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⟩