Adjoining elements to form subalgebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 = has_Inf.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 : A → A → Prop}
{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 (⇑(algebra_map R A) r₁) (⇑(algebra_map R A) r₂))
(Halg_left : ∀ (r : R) (x : A), x ∈ s → p (⇑(algebra_map R A) r) x)
(Halg_right : ∀ (r : R) (x : A), x ∈ s → p x (⇑(algebra_map 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 that it holds for x y ∈ s and that it satisfies a number of
natural properties.
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) :
theorem
algebra.span_le_adjoin
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : set A) :
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} :
⇑subalgebra.to_submodule (algebra.adjoin R s) ≤ 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)) :
@[simp]
theorem
algebra.adjoin_span
(R : Type u)
{A : Type v}
[comm_semiring 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 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) = subalgebra.map f (algebra.adjoin R s)
@[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 (has_insert.insert x ↑(algebra.adjoin R s)) = algebra.adjoin R (has_insert.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)
def
algebra.adjoin_comm_semiring_of_comm
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{s : set A}
(hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a) :
comm_semiring ↥(algebra.adjoin R s)
If all elements of s : set A commute pairwise, then adjoin R s is a commutative
semiring.
Equations
- algebra.adjoin_comm_semiring_of_comm R hcomm = {add := semiring.add (algebra.adjoin R s).to_semiring, add_assoc := _, zero := semiring.zero (algebra.adjoin R s).to_semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul (algebra.adjoin R s).to_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (algebra.adjoin R s).to_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one (algebra.adjoin R s).to_semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast (algebra.adjoin R s).to_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow (algebra.adjoin R s).to_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}
theorem
algebra.adjoin_singleton_one
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A] :
algebra.adjoin R {1} = ⊥
theorem
algebra.self_mem_adjoin_singleton
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(x : A) :
x ∈ algebra.adjoin R {x}
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_union_coe_submodule
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(s t : set A) :
⇑subalgebra.to_submodule (algebra.adjoin R (s ∪ t)) = ⇑subalgebra.to_submodule (algebra.adjoin R s) * ⇑subalgebra.to_submodule (algebra.adjoin R t)
theorem
algebra.adjoin_adjoin_of_tower
(R : Type u)
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[semiring B]
[algebra R B]
[algebra A B]
[is_scalar_tower R A B]
(s : set B) :
algebra.adjoin A ↑(algebra.adjoin R s) = algebra.adjoin A s
theorem
algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
[comm_semiring B]
[algebra R B]
[algebra A B]
[is_scalar_tower 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 : ⇑(algebra_map A B) r ∈ B') :
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)
def
algebra.adjoin_comm_ring_of_comm
(R : Type u)
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
{s : set A}
(hcomm : ∀ (a : A), a ∈ s → ∀ (b : A), b ∈ s → a * b = b * a) :
comm_ring ↥(algebra.adjoin R s)
If all elements of s : set A commute pairwise, then adjoin R s is a commutative
ring.
Equations
- algebra.adjoin_comm_ring_of_comm R hcomm = {add := ring.add (algebra.adjoin R s).to_ring, add_assoc := _, zero := ring.zero (algebra.adjoin R s).to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul (algebra.adjoin R s).to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (algebra.adjoin R s).to_ring, sub := ring.sub (algebra.adjoin R s).to_ring, sub_eq_add_neg := _, zsmul := ring.zsmul (algebra.adjoin R s).to_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast (algebra.adjoin R s).to_ring, nat_cast := ring.nat_cast (algebra.adjoin R s).to_ring, one := ring.one (algebra.adjoin R s).to_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul (algebra.adjoin R s).to_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow (algebra.adjoin R s).to_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
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) :
subalgebra.map φ (algebra.adjoin R s) = algebra.adjoin R (⇑φ '' s)