Adjoining elements to form subalgebras #
This file develops the basic theory of subalgebras of an R-algebra generated
by a set of elements. A basic interface for adjoin is set up.
Tags #
adjoin, algebra
theorem
Algebra.subset_adjoin
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
:
s ⊆ ↑(Algebra.adjoin R s)
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)
:
Algebra.adjoin R s ≤ S
theorem
Algebra.adjoin_eq_sInf
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
:
Algebra.adjoin R s = sInf {p | s ⊆ ↑p}
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}
:
Algebra.adjoin R s ≤ S ↔ s ⊆ ↑S
theorem
Algebra.adjoin_mono
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{t : Set A}
(H : s ⊆ t)
:
Algebra.adjoin R s ≤ Algebra.adjoin R t
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 ≤ Algebra.adjoin R s)
:
Algebra.adjoin R s = S
theorem
Algebra.adjoin_eq
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
Algebra.adjoin R ↑S = S
theorem
Algebra.adjoin_iUnion
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{α : Type u_1}
(s : α → Set A)
:
Algebra.adjoin R (Set.iUnion s) = ⨆ (i : α), Algebra.adjoin R (s i)
theorem
Algebra.adjoin_attach_biUnion
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[DecidableEq A]
{α : Type u_1}
{s : Finset α}
(f : { x // x ∈ s } → Finset A)
:
Algebra.adjoin R ↑(Finset.biUnion (Finset.attach s) f) = ⨆ (x : { x // x ∈ s }), Algebra.adjoin R ↑(f x)
theorem
Algebra.adjoin_induction
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{p : A → Prop}
{x : A}
(h : x ∈ Algebra.adjoin R s)
(Hs : (x : A) → x ∈ s → p x)
(Halg : (r : R) → p (↑(algebraMap R A) r))
(Hadd : (x y : A) → p x → p y → p (x + y))
(Hmul : (x y : A) → p x → p y → p (x * y))
:
p x
theorem
Algebra.adjoin_induction₂
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{p : A → A → Prop}
{a : A}
{b : A}
(ha : a ∈ Algebra.adjoin R s)
(hb : b ∈ Algebra.adjoin R s)
(Hs : (x : A) → x ∈ s → (y : A) → y ∈ s → p x y)
(Halg : (r₁ r₂ : R) → p (↑(algebraMap R A) r₁) (↑(algebraMap R A) r₂))
(Halg_left : (r : R) → (x : A) → x ∈ s → p (↑(algebraMap R A) r) x)
(Halg_right : (r : R) → (x : A) → x ∈ s → p x (↑(algebraMap R A) r))
(Hadd_left : (x₁ x₂ y : A) → p x₁ y → p x₂ y → p (x₁ + x₂) y)
(Hadd_right : (x y₁ y₂ : A) → p x y₁ → p x y₂ → p x (y₁ + y₂))
(Hmul_left : (x₁ x₂ y : A) → p x₁ y → p x₂ y → p (x₁ * x₂) y)
(Hmul_right : (x y₁ y₂ : A) → p x y₁ → p x y₂ → p x (y₁ * y₂))
:
p a b
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.
theorem
Algebra.adjoin_induction'
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
{p : { x // x ∈ Algebra.adjoin R s } → Prop}
(Hs : (x : A) → (h : x ∈ s) → p { val := x, property := (_ : x ∈ ↑(Algebra.adjoin R s)) })
(Halg : (r : R) → p (↑(algebraMap R { x // x ∈ Algebra.adjoin R s }) r))
(Hadd : (x y : { x // x ∈ Algebra.adjoin R s }) → p x → p y → p (x + y))
(Hmul : (x y : { x // x ∈ Algebra.adjoin R s }) → p x → p y → p (x * y))
(x : { x // x ∈ Algebra.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}
:
Algebra.adjoin R (Subtype.val ⁻¹' s) = ⊤
theorem
Algebra.adjoin_union
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set A)
(t : Set A)
:
Algebra.adjoin R (s ∪ t) = Algebra.adjoin R s ⊔ Algebra.adjoin R t
@[simp]
theorem
Algebra.adjoin_empty
(R : Type uR)
(A : Type uA)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
Algebra.adjoin R ∅ = ⊥
@[simp]
theorem
Algebra.adjoin_univ
(R : Type uR)
(A : Type uA)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
Algebra.adjoin R Set.univ = ⊤
theorem
Algebra.adjoin_eq_span
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set A)
:
↑Subalgebra.toSubmodule (Algebra.adjoin R s) = Submodule.span R ↑(Submonoid.closure s)
theorem
Algebra.span_le_adjoin
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set A)
:
Submodule.span R s ≤ ↑Subalgebra.toSubmodule (Algebra.adjoin R s)
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}
:
↑Subalgebra.toSubmodule (Algebra.adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t
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))
:
↑Subalgebra.toSubmodule (Algebra.adjoin R 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}
:
Algebra.adjoin R ↑(Submodule.span R s) = Algebra.adjoin R s
theorem
Algebra.adjoin_image
(R : Type uR)
{A : Type uA}
{B : Type uB}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
(f : A →ₐ[R] B)
(s : Set A)
:
Algebra.adjoin R (↑f '' s) = Subalgebra.map f (Algebra.adjoin R s)
@[simp]
theorem
Algebra.adjoin_insert_adjoin
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Set A)
(x : A)
:
Algebra.adjoin R (insert x ↑(Algebra.adjoin R s)) = Algebra.adjoin R (insert x s)
theorem
Algebra.adjoin_prod_le
(R : Type uR)
{A : Type uA}
{B : Type uB}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
(s : Set A)
(t : Set B)
:
Algebra.adjoin R (s ×ˢ t) ≤ Subalgebra.prod (Algebra.adjoin R s) (Algebra.adjoin R t)
theorem
Algebra.mem_adjoin_of_map_mul
(R : Type uR)
{A : Type uA}
{B : Type uB}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
{s : Set A}
{x : A}
{f : A →ₗ[R] B}
(hf : ∀ (a₁ a₂ : A), ↑f (a₁ * a₂) = ↑f a₁ * ↑f a₂)
(h : x ∈ Algebra.adjoin R s)
:
↑f x ∈ Algebra.adjoin R (↑f '' (s ∪ {1}))
theorem
Algebra.adjoin_inl_union_inr_eq_prod
(R : Type uR)
{A : Type uA}
{B : Type uB}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
(s : Set A)
(t : Set B)
:
Algebra.adjoin R (↑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ↑(LinearMap.inr R A B) '' (t ∪ {1})) = Subalgebra.prod (Algebra.adjoin R s) (Algebra.adjoin R t)
def
Algebra.adjoinCommSemiringOfComm
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{s : Set A}
(hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a)
:
CommSemiring { x // x ∈ Algebra.adjoin R s }
If all elements of s : Set A commute pairwise, then adjoin R s is a commutative
semiring.
Instances For
theorem
Algebra.adjoin_singleton_one
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
Algebra.adjoin R {1} = ⊥
theorem
Algebra.self_mem_adjoin_singleton
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(x : A)
:
x ∈ Algebra.adjoin R {x}
theorem
Algebra.adjoin_algebraMap
(R : Type uR)
{S : Type uS}
(A : Type uA)
[CommSemiring R]
[CommSemiring S]
[Semiring A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
(s : Set S)
:
Algebra.adjoin R (↑(algebraMap S A) '' s) = Subalgebra.map (IsScalarTower.toAlgHom R S A) (Algebra.adjoin R s)
theorem
Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin
(R : Type uR)
{S : Type uS}
{A : Type uA}
[CommSemiring R]
[CommSemiring S]
[Semiring A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
(s : Set S)
(t : Set A)
:
Algebra.adjoin R (↑(algebraMap S A) '' s ∪ t) = Subalgebra.restrictScalars R (Algebra.adjoin { x // x ∈ Algebra.adjoin R s } t)
theorem
Algebra.adjoin_adjoin_of_tower
(R : Type uR)
{S : Type uS}
{A : Type uA}
[CommSemiring R]
[CommSemiring S]
[Semiring A]
[Algebra R S]
[Algebra R A]
[Algebra S A]
[IsScalarTower R S A]
(s : Set A)
:
Algebra.adjoin S ↑(Algebra.adjoin R s) = Algebra.adjoin S s
@[simp]
theorem
Algebra.adjoin_top
(R : Type uR)
{S : Type uS}
{A : Type uA}
[CommSemiring R]
[CommSemiring S]
[Semiring A]
[Algebra R S]
[Algebra S A]
{t : Set A}
:
Algebra.adjoin { x // x ∈ ⊤ } t = Subalgebra.restrictScalars { x // x ∈ ⊤ } (Algebra.adjoin S t)
theorem
Algebra.adjoin_union_eq_adjoin_adjoin
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(s : Set A)
(t : Set A)
:
Algebra.adjoin R (s ∪ t) = Subalgebra.restrictScalars R (Algebra.adjoin { x // x ∈ Algebra.adjoin R s } t)
theorem
Algebra.adjoin_union_coe_submodule
(R : Type uR)
{A : Type uA}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(s : Set A)
(t : Set A)
:
↑Subalgebra.toSubmodule (Algebra.adjoin R (s ∪ t)) = ↑Subalgebra.toSubmodule (Algebra.adjoin R s) * ↑Subalgebra.toSubmodule (Algebra.adjoin R t)
theorem
Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin
{R : Type uR}
{A : Type uA}
{B : Type uB}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
[CommSemiring B]
[Algebra R B]
[Algebra A B]
[IsScalarTower R A B]
(r : A)
(s : Set B)
(B' : Subalgebra R B)
(hs : r • s ⊆ ↑B')
{x : B}
(hx : x ∈ Algebra.adjoin R s)
(hr : ↑(algebraMap A B) r ∈ B')
:
theorem
Algebra.pow_smul_mem_adjoin_smul
{R : Type uR}
{A : Type uA}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(r : R)
(s : Set A)
{x : A}
(hx : x ∈ Algebra.adjoin R s)
:
theorem
Algebra.mem_adjoin_iff
{R : Type uR}
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{s : Set A}
{x : A}
:
x ∈ Algebra.adjoin R s ↔ x ∈ Subring.closure (Set.range ↑(algebraMap R A) ∪ s)
theorem
Algebra.adjoin_eq_ring_closure
{R : Type uR}
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
(s : Set A)
:
Subalgebra.toSubring (Algebra.adjoin R s) = Subring.closure (Set.range ↑(algebraMap R A) ∪ s)
def
Algebra.adjoinCommRingOfComm
(R : Type uR)
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{s : Set A}
(hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a)
:
CommRing { x // x ∈ Algebra.adjoin R s }
If all elements of s : Set A commute pairwise, then adjoin R s is a commutative
ring.
Instances For
theorem
AlgHom.map_adjoin
{R : Type uR}
{A : Type uA}
{B : Type uB}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
(φ : A →ₐ[R] B)
(s : Set A)
:
Subalgebra.map φ (Algebra.adjoin R s) = Algebra.adjoin R (↑φ '' s)
theorem
AlgHom.adjoin_le_equalizer
{R : Type uR}
{A : Type uA}
{B : Type uB}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Algebra R A]
[Algebra R B]
(φ₁ : A →ₐ[R] B)
(φ₂ : A →ₐ[R] B)
{s : Set A}
(h : Set.EqOn (↑φ₁) (↑φ₂) s)
:
Algebra.adjoin R s ≤ AlgHom.equalizer φ₁ φ₂
def
Subsemiring.closureEquivAdjoinNat
{R : Type u_1}
[Semiring R]
(s : Set R)
:
{ x // x ∈ Subsemiring.closure s } ≃ₐ[ℕ] { x // x ∈ Algebra.adjoin ℕ s }
The ℕ-algebra equivalence between Subsemiring.closure s and Algebra.adjoin ℕ s given
by the identity map.
Instances For
def
Subring.closureEquivAdjoinInt
{R : Type u_1}
[Ring R]
(s : Set R)
:
{ x // x ∈ Subring.closure s } ≃ₐ[ℤ] { x // x ∈ Algebra.adjoin ℤ s }
The ℤ-algebra equivalence between Subring.closure s and Algebra.adjoin ℤ s given by
the identity map.