Mathlib.Algebra.Algebra.Subalgebra.Directed

Module docstring

{"# 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. "}

Subalgebra.coe_iSup_of_directed theorem

(dir : Directed (· ≤ ·) K) : ↑(iSup K) = ⋃ i, (K i : Set A)

Full source

theorem coe_iSup_of_directed (dir : Directed (· ≤ ·) K) : ↑(iSup K) = ⋃ i, (K i : Set A) :=
  let s : Subalgebra R A :=
    { __ := Subsemiring.copy _ _ (Subsemiring.coe_iSup_of_directed dir).symm
      algebraMap_mem' := fun _ ↦ Set.mem_iUnion.2
        ⟨Classical.arbitrary ι, Subalgebra.algebraMap_mem _ _⟩ }
  have : iSup K = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)
  this.symm ▸ rfl

Supremum of Directed Family of Subalgebras Equals Union of Their Underlying Sets

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. Given a directed family $(K_i)_{i \in \iota}$ of subalgebras of $A$ with respect to inclusion, the underlying set of the supremum $\bigsqcup_{i \in \iota} K_i$ is equal to the union $\bigcup_{i \in \iota} K_i$ of the underlying sets of the subalgebras $K_i$.

Subalgebra.iSupLift definition

 (dir : Directed (· ≤ ·) 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

Full source

/-- 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. -/
noncomputable def iSupLift (dir : Directed (· ≤ ·) 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 :=
  { toFun := Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x)
        (fun i j x hxi hxj => by
          let ⟨k, hik, hjk⟩ := dir i j
          dsimp
          rw [hf i k hik, hf j k hjk]
          rfl)
        (T : Set A) (by rw [hT, coe_iSup_of_directed dir])
    map_one' := by apply Set.iUnionLift_const _ (fun _ => 1) <;> simp
    map_zero' := by dsimp; apply Set.iUnionLift_const _ (fun _ => 0) <;> simp
    map_mul' := by
      subst hT; dsimp
      apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
      all_goals simp
    map_add' := by
      subst hT; dsimp
      apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
      all_goals simp
    commutes' := fun r => by
      dsimp
      apply Set.iUnionLift_const _ (fun _ => algebraMap R _ r) <;> simp }

Lifting homomorphism to directed supremum of subalgebras

Informal description

Given a directed family $(K_i)_{i \in \iota}$ of subalgebras of an $R$-algebra $A$, a family of $R$-algebra homomorphisms $f_i \colon K_i \to B$ that agree on pairwise intersections (i.e., for any $i, j \in \iota$ with $K_i \subseteq K_j$, $f_i = f_j \circ \text{inclusion}(K_i \subseteq K_j)$), and a subalgebra $T = \bigsqcup_{i \in \iota} K_i$, the function $\text{iSupLift}$ constructs an $R$-algebra homomorphism $T \to B$ by lifting the $f_i$ to the supremum. Specifically, for $x \in T$, $\text{iSupLift}$ selects an index $i$ such that $x \in K_i$ and returns $f_i(x)$. This homomorphism preserves addition, multiplication, and the action of $R$.

Subalgebra.iSupLift_inclusion theorem

 {dir : Directed (· ≤ ·) 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

Full source

@[simp]
theorem iSupLift_inclusion {dir : Directed (· ≤ ·) 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 := by
  dsimp [iSupLift, inclusion]
  rw [Set.iUnionLift_inclusion]

Compatibility of Lifted Homomorphism with Inclusion in Directed Union of Subalgebras

Informal description

Let $R$ be a commutative semiring, $A$ and $B$ be $R$-algebras, and $(K_i)_{i \in \iota}$ be a directed family of subalgebras of $A$ with respect to inclusion. Given a family of $R$-algebra homomorphisms $f_i \colon K_i \to B$ that are compatible on intersections (i.e., $f_i = f_j \circ \text{inclusion}(K_i \subseteq K_j)$ whenever $K_i \subseteq K_j$), and a subalgebra $T = \bigsqcup_{i \in \iota} K_i$, then for any $i \in \iota$ and $x \in K_i$ with $K_i \subseteq T$, the lifted homomorphism satisfies $\text{iSupLift}(K, f, T)(\text{inclusion}(h)(x)) = f_i(x)$, where $\text{inclusion}(h)$ is the canonical inclusion of $K_i$ into $T$.

Subalgebra.iSupLift_comp_inclusion theorem

 {dir : Directed (· ≤ ·) 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

Full source

@[simp]
theorem iSupLift_comp_inclusion {dir : Directed (· ≤ ·) 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 := by ext; simp

Compatibility of Lifted Homomorphism with Inclusion in Directed Union of Subalgebras

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. Given a directed family $(K_i)_{i \in \iota}$ of subalgebras of $A$ with respect to inclusion, a family of $R$-algebra homomorphisms $f_i \colon K_i \to B$ that are compatible on intersections (i.e., $f_i = f_j \circ \text{inclusion}(K_i \subseteq K_j)$ whenever $K_i \subseteq K_j$), and a subalgebra $T = \bigsqcup_{i \in \iota} K_i$, then for any $i \in \iota$ and any inclusion $h \colon K_i \hookrightarrow T$, the composition of the lifted homomorphism $\text{iSupLift}(K, f, T)$ with $\text{inclusion}(h)$ equals $f_i$.

Subalgebra.iSupLift_mk theorem

 {dir : Directed (· ≤ ·) 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 : A) ∈ T) : iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x

Full source

@[simp]
theorem iSupLift_mk {dir : Directed (· ≤ ·) 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 : A) ∈ T) :
    iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x := by
  dsimp [iSupLift, inclusion]
  rw [Set.iUnionLift_mk]

Value of Lifted Homomorphism on Elements from Component Subalgebras

Informal description

Let $R$ be a commutative semiring and $A$, $B$ be semirings equipped with $R$-algebra structures. Given a directed family of subalgebras $(K_i)_{i \in \iota}$ of $A$, a family of $R$-algebra homomorphisms $f_i \colon K_i \to B$ that agree on pairwise intersections (i.e., $f_i = f_j \circ \text{inclusion}(K_i \subseteq K_j)$ whenever $K_i \leq K_j$), and a subalgebra $T = \bigsqcup_{i \in \iota} K_i$, then for any $x \in K_i$ such that $x \in T$, the lifted homomorphism satisfies $\text{iSupLift}(K, f, hf, T, hT)(x) = f_i(x)$.

Subalgebra.iSupLift_of_mem theorem

 {dir : Directed (· ≤ ·) 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 : A) ∈ K i) : iSupLift K dir f hf T hT x = f i ⟨x, hx⟩

Full source

theorem iSupLift_of_mem {dir : Directed (· ≤ ·) 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 : A) ∈ K i) :
    iSupLift K dir f hf T hT x = f i ⟨x, hx⟩ := by
  dsimp [iSupLift, inclusion]
  rw [Set.iUnionLift_of_mem]

Value of Lifted Homomorphism on Directed Union of Subalgebras

Informal description

Let $R$ be a commutative semiring and $A$, $B$ be semirings equipped with $R$-algebra structures. Let $(K_i)_{i \in \iota}$ be a directed family of subalgebras of $A$ with respect to inclusion, and let $f_i \colon K_i \to B$ be a family of $R$-algebra homomorphisms that agree on pairwise intersections (i.e., $f_i = f_j \circ \text{inclusion}(K_i \subseteq K_j)$ whenever $K_i \subseteq K_j$). Let $T = \bigsqcup_{i \in \iota} K_i$ be the supremum of the family. For any $x \in T$ and any index $i \in \iota$ such that $x \in K_i$, the lifted homomorphism $\text{iSupLift}(K, f, T, hT)(x)$ equals $f_i(x)$.