Complete lattice structure of subalgebras #
In this file we define Algebra.adjoin and the complete lattice structure on subalgebras.
More lemmas about adjoin can be found in Mathlib.RingTheory.Adjoin.Basic.
def
Algebra.adjoin
(R : Type u)
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set A)
:
Subalgebra R A
The minimal subalgebra that includes s.
Equations
- Algebra.adjoin R s = { toSubsemiring := Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s), algebraMap_mem' := ⋯ }
Instances For
@[simp]
theorem
Algebra.adjoin_toSubsemiring
(R : Type u)
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set A)
:
Galois insertion between adjoin and coe.
Equations
- Algebra.gi = { choice := fun (s : Set A) (hs : ↑(Algebra.adjoin R s) ≤ s) => (Algebra.adjoin R s).copy s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
instance
Algebra.instCompleteLatticeSubalgebra
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
CompleteLattice (Subalgebra R A)
Equations
- One or more equations did not get rendered due to their size.
theorem
Algebra.sup_def
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S T : Subalgebra R A)
:
theorem
Algebra.sSup_def
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Set (Subalgebra R A))
:
@[simp]
@[simp]
theorem
Algebra.mem_top
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{x : A}
:
@[simp]
theorem
Algebra.top_toSubmodule
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
@[simp]
theorem
Algebra.top_toSubsemiring
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
@[simp]
theorem
Algebra.toSubmodule_eq_top
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S : Subalgebra R A}
:
@[simp]
theorem
Algebra.toSubsemiring_eq_top
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S : Subalgebra R A}
:
theorem
Algebra.mem_sup_left
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S T : Subalgebra R A}
{x : A}
:
theorem
Algebra.mem_sup_right
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S T : Subalgebra R A}
{x : A}
:
theorem
Algebra.mul_mem_sup
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S T : Subalgebra R A}
{x y : A}
(hx : x ∈ S)
(hy : y ∈ T)
:
theorem
Algebra.map_sup
{R : Type u}
{A : Type v}
{B : Type w}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
(f : A →ₐ[R] B)
(S T : Subalgebra R A)
:
theorem
Algebra.map_inf
{R : Type u}
{A : Type v}
{B : Type w}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
(f : A →ₐ[R] B)
(hf : Function.Injective ⇑f)
(S T : Subalgebra R A)
:
@[simp]
theorem
Algebra.coe_inf
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S T : Subalgebra R A)
:
@[simp]
theorem
Algebra.mem_inf
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S T : Subalgebra R A}
{x : A}
:
@[simp]
theorem
Algebra.inf_toSubmodule
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S T : Subalgebra R A)
:
@[simp]
theorem
Algebra.inf_toSubsemiring
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S T : Subalgebra R A)
:
@[simp]
theorem
Algebra.sup_toSubsemiring
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S T : Subalgebra R A)
:
@[simp]
theorem
Algebra.coe_sInf
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Set (Subalgebra R A))
:
theorem
Algebra.mem_sInf
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S : Set (Subalgebra R A)}
{x : A}
:
@[simp]
theorem
Algebra.sInf_toSubmodule
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Set (Subalgebra R A))
:
@[simp]
theorem
Algebra.sInf_toSubsemiring
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Set (Subalgebra R A))
:
@[simp]
theorem
Algebra.sSup_toSubsemiring
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Set (Subalgebra R A))
(hS : S.Nonempty)
:
@[simp]
theorem
Algebra.coe_iInf
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{ι : Sort u_1}
{S : ι → Subalgebra R A}
:
theorem
Algebra.mem_iInf
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{ι : Sort u_1}
{S : ι → Subalgebra R A}
{x : A}
:
theorem
Algebra.map_iInf
{R : Type u}
{A : Type v}
{B : Type w}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
{ι : Sort u_1}
[Nonempty ι]
(f : A →ₐ[R] B)
(hf : Function.Injective ⇑f)
(s : ι → Subalgebra R A)
:
@[simp]
theorem
Algebra.iInf_toSubmodule
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{ι : Sort u_1}
(S : ι → Subalgebra R A)
:
@[simp]
theorem
Algebra.iInf_toSubsemiring
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{ι : Sort u_1}
(S : ι → Subalgebra R A)
:
@[simp]
theorem
Algebra.iSup_toSubsemiring
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{ι : Sort u_1}
[Nonempty ι]
(S : ι → Subalgebra R A)
:
theorem
Algebra.mem_iSup_of_mem
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{ι : Sort u_1}
{S : ι → Subalgebra R A}
(i : ι)
{x : A}
(hx : x ∈ S i)
:
theorem
Algebra.iSup_induction
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{ι : Sort u_1}
(S : ι → Subalgebra R A)
{motive : A → Prop}
{x : A}
(mem : x ∈ ⨆ (i : ι), S i)
(basic : ∀ (i : ι), ∀ a ∈ S i, motive a)
(zero : motive 0)
(one : motive 1)
(add : ∀ (a b : A), motive a → motive b → motive (a + b))
(mul : ∀ (a b : A), motive a → motive b → motive (a * b))
(algebraMap : ∀ (r : R), motive ((algebraMap R A) r))
:
motive x
theorem
Algebra.iSup_induction'
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{ι : Sort u_1}
(S : ι → Subalgebra R A)
{motive : (x : A) → x ∈ ⨆ (i : ι), S i → Prop}
{x : A}
(mem : x ∈ ⨆ (i : ι), S i)
(basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯)
(zero : motive 0 ⋯)
(one : motive 1 ⋯)
(add : ∀ (x y : A) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), motive x hx → motive y hy → motive (x + y) ⋯)
(mul : ∀ (x y : A) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), motive x hx → motive y hy → motive (x * y) ⋯)
(algebraMap : ∀ (r : R), motive ((algebraMap R A) r) ⋯)
:
motive x mem
A dependent version of Subalgebra.iSup_induction.
instance
Algebra.instInhabitedSubalgebra
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
Inhabited (Subalgebra R A)
Equations
- Algebra.instInhabitedSubalgebra = { default := ⊥ }
theorem
Algebra.mem_bot
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{x : A}
:
theorem
Algebra.toSubmodule_bot
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
TODO: change proof to rfl when fixing https://github.com/leanprover-community/mathlib4/issues/18110.
@[simp]
theorem
Algebra.eq_top_iff
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S : Subalgebra R A}
:
@[deprecated AlgHom.range_eq_top (since := "2024-11-11")]
theorem
Algebra.range_top_iff_surjective
{R : Type u}
{A : Type v}
{B : Type w}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
(f : A →ₐ[R] B)
:
Alias of AlgHom.range_eq_top.
theorem
Algebra.surjective_algebraMap_iff
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
theorem
Algebra.bijective_algebraMap_iff
{R : Type u_1}
{A : Type u_2}
[Field R]
[Semiring A]
[Nontrivial A]
[Algebra R A]
:
noncomputable def
Algebra.botEquivOfInjective
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(h : Function.Injective ⇑(algebraMap R A))
:
The bottom subalgebra is isomorphic to the base ring.
Equations
Instances For
noncomputable def
Algebra.botEquiv
(F : Type u_1)
(R : Type u_2)
[Field F]
[Semiring R]
[Nontrivial R]
[Algebra F R]
:
The bottom subalgebra is isomorphic to the field.
Equations
Instances For
The top subalgebra is isomorphic to the algebra.
This is the algebra version of Submodule.topEquiv.
Equations
Instances For
@[simp]
theorem
Subalgebra.topEquiv_symm_apply_coe
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(a : A)
:
@[simp]
theorem
Subalgebra.topEquiv_apply
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(a : ↥⊤)
:
instance
AlgHom.subsingleton
{R : Type u}
{A : Type v}
{B : Type w}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Subsingleton (Subalgebra R A)]
:
Subsingleton (A →ₐ[R] B)
instance
AlgEquiv.subsingleton_left
{R : Type u}
{A : Type v}
{B : Type w}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Subsingleton (Subalgebra R A)]
:
Subsingleton (A ≃ₐ[R] B)
instance
AlgEquiv.subsingleton_right
{R : Type u}
{A : Type v}
{B : Type w}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Subsingleton (Subalgebra R B)]
:
Subsingleton (A ≃ₐ[R] B)
Equations
- Subalgebra.instUnique = { toInhabited := inferInstanceAs (Inhabited (Subalgebra R R)), uniq := ⋯ }
@[simp]
theorem
Subalgebra.center_eq_top
(R : Type u)
[CommSemiring R]
(A : Type u_1)
[CommSemiring A]
[Algebra R A]
:
@[simp]
theorem
Subalgebra.centralizer_eq_top_iff_subset
(R : Type u)
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
:
theorem
AlgHom.eqOn_sup
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
{F : Type u_4}
[FunLike F A B]
[AlgHomClass F R A B]
{φ ψ : F}
{S T : Subalgebra R A}
(hS : Set.EqOn ⇑φ ⇑ψ ↑S)
(hT : Set.EqOn ⇑φ ⇑ψ ↑T)
:
theorem
AlgHom.ext_on_codisjoint
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
{F : Type u_4}
[FunLike F A B]
[AlgHomClass F R A B]
{φ ψ : F}
{S T : Subalgebra R A}
(hST : Codisjoint S T)
(hS : Set.EqOn ⇑φ ⇑ψ ↑S)
(hT : Set.EqOn ⇑φ ⇑ψ ↑T)
:
theorem
Subalgebra.map_comap_eq_self_of_surjective
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
{f : A →ₐ[R] B}
(hf : Function.Surjective ⇑f)
(S : Subalgebra R B)
:
theorem
Algebra.subset_adjoin
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
:
theorem
Algebra.adjoin_le
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{S : Subalgebra R A}
(H : s ⊆ ↑S)
:
theorem
Algebra.adjoin_singleton_le
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S : Subalgebra R A}
{a : A}
(H : a ∈ S)
:
theorem
Algebra.adjoin_le_iff
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{S : Subalgebra R A}
:
theorem
Algebra.adjoin_eq_of_le
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
(S : Subalgebra R A)
(h₁ : s ⊆ ↑S)
(h₂ : S ≤ adjoin R s)
:
theorem
Algebra.adjoin_eq
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
theorem
Algebra.adjoin_iUnion
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{α : Type u_1}
(s : α → Set A)
:
theorem
Algebra.adjoin_induction
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{p : (x : A) → x ∈ adjoin R s → Prop}
(mem : ∀ (x : A) (hx : x ∈ s), p x ⋯)
(algebraMap : ∀ (r : R), p ((algebraMap R A) r) ⋯)
(add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯)
(mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯)
{x : A}
(hx : x ∈ adjoin R s)
:
p x hx
theorem
Algebra.adjoin_induction₂
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop}
(mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯)
(algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯)
(algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯)
(algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯)
(add_left :
∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz)
(add_right :
∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
p x y hx hy → p x z hx hz → p x (y + z) hx ⋯)
(mul_left :
∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz)
(mul_right :
∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
p x y hx hy → p x z hx hz → p x (y * z) hx ⋯)
{x y : A}
(hx : x ∈ adjoin R s)
(hy : y ∈ adjoin R s)
:
p x y hx hy
Induction principle for the algebra generated by a set s: show that p x y holds for any
x y ∈ adjoin R s given that it holds for x y ∈ s and that it satisfies a number of
natural properties.
@[deprecated Algebra.adjoin_induction (since := "2024-10-11")]
theorem
Algebra.adjoin_induction'
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{p : ↥(adjoin R s) → Prop}
(mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩)
(algebraMap : ∀ (r : R), p ((algebraMap R ↥(adjoin R s)) r))
(add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y))
(mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y))
(x : ↥(adjoin R s))
:
p x
The difference with Algebra.adjoin_induction is that this acts on the subtype.
@[simp]
theorem
Algebra.adjoin_adjoin_coe_preimage
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
:
@[simp]
theorem
Algebra.adjoin_singleton_algebraMap
{R : Type uR}
(A : Type uA)
[CommSemiring R]
[Semiring A]
[Algebra R A]
(x : R)
:
@[simp]
theorem
Algebra.adjoin_insert_algebraMap
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(x : R)
(s : Set A)
:
theorem
Algebra.adjoin_eq_span
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set A)
:
theorem
Algebra.span_le_adjoin
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set A)
:
theorem
Algebra.adjoin_toSubmodule_le
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{t : Submodule R A}
:
theorem
Algebra.adjoin_eq_span_of_subset
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
(hs : ↑(Submonoid.closure s) ⊆ ↑(Submodule.span R s))
:
@[simp]
theorem
Algebra.adjoin_span
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
:
theorem
Algebra.adjoin_le_centralizer_centralizer
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set A)
:
@[reducible, inline]
abbrev
Algebra.adjoinCommSemiringOfComm
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
(hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a)
:
CommSemiring ↥(adjoin R s)
If all elements of s : Set A commute pairwise, then adjoin s is a commutative semiring.
Equations
- Algebra.adjoinCommSemiringOfComm R hcomm = { toSemiring := (Algebra.adjoin R s).toSemiring, mul_comm := ⋯ }
Instances For
theorem
Algebra.adjoin_union_coe_submodule
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(s t : Set A)
:
Subalgebra.toSubmodule (adjoin R (s ∪ t)) = Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)
@[reducible, inline]
abbrev
Algebra.adjoinCommRingOfComm
(R : Type uR)
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{s : Set A}
(hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a)
:
If all elements of s : Set A commute pairwise, then adjoin R s is a commutative
ring.
Equations
- Algebra.adjoinCommRingOfComm R hcomm = { toRing := (Algebra.adjoin R s).toRing, mul_comm := ⋯ }
Instances For
theorem
AlgHom.ext_of_eq_adjoin
{R : Type uR}
{A : Type uA}
{B : Type uB}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
{S : Subalgebra R A}
{s : Set A}
(hS : S = Algebra.adjoin R s)
⦃φ₁ φ₂ : ↥S →ₐ[R] B⦄
(h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩)
:
The ℕ-algebra equivalence between Subsemiring.closure s and Algebra.adjoin ℕ s given
by the identity map.
Equations
Instances For
The ℤ-algebra equivalence between Subring.closure s and Algebra.adjoin ℤ s given by
the identity map.
Equations
Instances For
theorem
Submonoid.adjoin_eq_span_of_eq_span
(F : Type u_1)
(E : Type u_2)
{K : Type u_3}
[CommSemiring E]
[Semiring K]
[SMul F E]
[Algebra E K]
[Semiring F]
[Module F K]
[IsScalarTower F E K]
(L : Submonoid K)
{S : Set K}
(h : ↑L = ↑(Submodule.span F S))
:
If K / E / F is a ring extension tower, L is a submonoid of K / F which is generated by
S as an F-module, then E[L] is generated by S as an E-module.
theorem
Subalgebra.adjoin_eq_span_of_eq_span
{F : Type u_1}
(E : Type u_2)
{K : Type u_3}
[CommSemiring E]
[Semiring K]
[SMul F E]
[Algebra E K]
[CommSemiring F]
[Algebra F K]
[IsScalarTower F E K]
(L : Subalgebra F K)
{S : Set K}
(h : toSubmodule L = Submodule.span F S)
:
If K / E / F is a ring extension tower, L is a subalgebra of K / F which is generated by
S as an F-module, then E[L] is generated by S as an E-module.
theorem
NonUnitalAlgebra.adjoin_le_algebra_adjoin
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Ring A]
[Algebra R A]
(s : Set A)
:
theorem
Algebra.adjoin_nonUnitalSubalgebra
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Ring A]
[Algebra R A]
(s : Set A)
: