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 u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A} :
s ⊆ ↑(algebra.adjoin R s)
theorem
algebra.adjoin_le
{R : Type u}
{A : Type v}
[comm_semiring 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_Inf
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A} :
algebra.adjoin R s = Inf {p : subalgebra R A | s ⊆ ↑p}
theorem
algebra.adjoin_le_iff
{R : Type u}
{A : Type v}
[comm_semiring 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 u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s t : set A}
(H : s ⊆ t) :
algebra.adjoin R s ≤ algebra.adjoin R t
theorem
algebra.adjoin_eq_of_le
{R : Type u}
{A : Type v}
[comm_semiring 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 u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(S : subalgebra R A) :
algebra.adjoin R ↑S = S
theorem
algebra.adjoin_Union
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{α : Type u_1}
(s : α → set A) :
algebra.adjoin R (set.Union s) = ⨆ (i : α), algebra.adjoin R (s i)
theorem
algebra.adjoin_attach_bUnion
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
[decidable_eq A]
{α : Type u_1}
{s : finset α}
(f : ↥s → finset A) :
algebra.adjoin R ↑(s.attach.bUnion f) = ⨆ (x : ↥s), algebra.adjoin R ↑(f x)
theorem
algebra.adjoin_induction
{R : Type u}
{A : Type v}
[comm_semiring 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 (⇑(algebra_map 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 u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A}
{p : ↥(algebra.adjoin R s) → Prop}
(Hs : ∀ (x : A) (h : x ∈ s), p ⟨x, _⟩)
(Halg : ∀ (r : R), p (⇑(algebra_map R ↥(algebra.adjoin R s)) r))
(Hadd : ∀ (x y : ↥(algebra.adjoin R s)), p x → p y → p (x + y))
(Hmul : ∀ (x y : ↥(algebra.adjoin R s)), p x → p y → p (x * y))
(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 u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A} :
algebra.adjoin R (coe ⁻¹' s) = ⊤
theorem
algebra.adjoin_union
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s t : set A) :
algebra.adjoin R (s ∪ t) = algebra.adjoin R s ⊔ algebra.adjoin R t
@[simp]
theorem
algebra.adjoin_empty
(R : Type u)
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A] :
algebra.adjoin R ∅ = ⊥
@[simp]
theorem
algebra.adjoin_univ
(R : Type u)
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A] :
theorem
algebra.adjoin_eq_span
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : set A) :
(algebra.adjoin R s).to_submodule = submodule.span R ↑(submonoid.closure s)
theorem
algebra.span_le_adjoin
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : set A) :
submodule.span R s ≤ (algebra.adjoin R s).to_submodule
theorem
algebra.adjoin_to_submodule_le
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A}
{t : submodule R A} :
(algebra.adjoin R s).to_submodule ≤ t ↔ ↑(submonoid.closure s) ⊆ ↑t
theorem
algebra.adjoin_eq_span_of_subset
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A}
(hs : ↑(submonoid.closure s) ⊆ ↑(submodule.span R s)) :
(algebra.adjoin R s).to_submodule = submodule.span R s
theorem
algebra.adjoin_image
(R : Type u)
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(f : A →ₐ[R] B)
(s : set A) :
algebra.adjoin R (⇑f '' s) = (algebra.adjoin R s).map f
@[simp]
theorem
algebra.adjoin_insert_adjoin
(R : Type u)
{A : Type v}
[comm_semiring 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 u)
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(s : set A)
(t : set B) :
algebra.adjoin R (s ×ˢ t) ≤ (algebra.adjoin R s).prod (algebra.adjoin R t)
theorem
algebra.adjoin_inl_union_inr_eq_prod
(R : Type u)
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(s : set A)
(t : set B) :
algebra.adjoin R (⇑(linear_map.inl R A B) '' (s ∪ {1}) ∪ ⇑(linear_map.inr R A B) '' (t ∪ {1})) = (algebra.adjoin R s).prod (algebra.adjoin R t)
theorem
algebra.adjoin_union_eq_adjoin_adjoin
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(s t : set A) :
algebra.adjoin R (s ∪ t) = subalgebra.restrict_scalars R (algebra.adjoin ↥(algebra.adjoin R s) t)
theorem
algebra.adjoin_singleton_one
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A] :
algebra.adjoin R {1} = ⊥
theorem
algebra.adjoin_union_coe_submodule
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(s t : set A) :
(algebra.adjoin R (s ∪ t)).to_submodule = ((algebra.adjoin R s).to_submodule) * (algebra.adjoin R t).to_submodule
theorem
algebra.pow_smul_mem_adjoin_smul
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(r : R)
(s : set A)
{x : A}
(hx : x ∈ algebra.adjoin R s) :
theorem
algebra.mem_adjoin_iff
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
{s : set A}
{x : A} :
x ∈ algebra.adjoin R s ↔ x ∈ subring.closure (set.range ⇑(algebra_map R A) ∪ s)
theorem
algebra.adjoin_eq_ring_closure
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(s : set A) :
(algebra.adjoin R s).to_subring = subring.closure (set.range ⇑(algebra_map R A) ∪ s)
theorem
alg_hom.map_adjoin
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(φ : A →ₐ[R] B)
(s : set A) :
(algebra.adjoin R s).map φ = algebra.adjoin R (⇑φ '' s)