Documentation

Mathlib.RingTheory.Adjoin.Basic

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) :
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 : Subalgebra R A | 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) :
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) :
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 (s.attach.biUnion 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 : AProp} {x : A} (h : x Algebra.adjoin R s) (mem : xs, p x) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r)) (add : ∀ (x y : A), p xp yp (x + y)) (mul : ∀ (x y : A), p xp yp (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 : AAProp} {a : A} {b : A} (ha : a Algebra.adjoin R s) (hb : b Algebra.adjoin R s) (Hs : xs, ys, p x y) (Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)) (Halg_left : ∀ (r : R), xs, p ((algebraMap R A) r) x) (Halg_right : ∀ (r : R), xs, p x ((algebraMap R A) r)) (Hadd_left : ∀ (x₁ x₂ y : A), p x₁ yp x₂ yp (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₁ yp x₂ yp (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 : (Algebra.adjoin R s)Prop} (mem : ∀ (x : A) (h : x s), p x, ) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R (Algebra.adjoin R s)) r)) (add : ∀ (x y : (Algebra.adjoin R s)), p xp yp (x + y)) (mul : ∀ (x y : (Algebra.adjoin R s)), p xp yp (x * y)) (x : (Algebra.adjoin R s)) :
p x

The difference with Algebra.adjoin_induction is that this acts on the subtype.

theorem Algebra.adjoin_induction'' {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {x : A} (hx : x Algebra.adjoin R s) {p : (x : A) → x Algebra.adjoin R sProp} (mem : ∀ (x : A) (h : x s), p x ) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ) (add : ∀ (x : A) (hx : x Algebra.adjoin R s) (y : A) (hy : y Algebra.adjoin R s), p x hxp y hyp (x + y) ) (mul : ∀ (x : A) (hx : x Algebra.adjoin R s) (y : A) (hy : y Algebra.adjoin R s), p x hxp y hyp (x * y) ) :
p x hx
@[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) :
@[simp]
theorem Algebra.adjoin_empty (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] :
@[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} :
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) :
@[simp]
theorem Algebra.adjoin_insert_adjoin (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) (x : A) :
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) :
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})) = (Algebra.adjoin R s).prod (Algebra.adjoin R t)
def Algebra.adjoinCommSemiringOfComm (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} (hcomm : as, bs, a * b = b * a) :

If all elements of s : Set A commute pairwise, then adjoin R s is a commutative semiring.

Equations
Instances For
    theorem Algebra.commute_of_mem_adjoin_of_forall_mem_commute {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} {b : A} {s : Set A} (hb : b Algebra.adjoin R s) (h : bs, Commute a b) :
    theorem Algebra.commute_of_mem_adjoin_singleton_of_commute {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} {b : A} {c : A} (hc : c Algebra.adjoin R {b}) (h : Commute a b) :
    theorem Algebra.commute_of_mem_adjoin_self {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} {b : A} (hb : b Algebra.adjoin R {a}) :
    theorem Algebra.self_mem_adjoin_singleton (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :
    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) :
    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) :
    @[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} :
    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') :
    ∃ (n₀ : ), nn₀, r ^ n x 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) :
    ∃ (n₀ : ), nn₀, r ^ n x Algebra.adjoin R (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} :
    theorem Algebra.adjoin_eq_ring_closure {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (s : Set A) :
    def Algebra.adjoinCommRingOfComm (R : Type uR) {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {s : Set A} (hcomm : as, bs, a * b = b * a) :

    If all elements of s : Set A commute pairwise, then adjoin R s is a commutative ring.

    Equations
    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) :
      @[simp]
      theorem AlgHom.map_adjoin_singleton {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A →ₐ[R] B) (x : A) :
      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 φ₁.equalizer φ₂
      theorem AlgHom.ext_of_adjoin_eq_top {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {s : Set A} (h : Algebra.adjoin R s = ) ⦃φ₁ : A →ₐ[R] B ⦃φ₂ : A →ₐ[R] B (hs : Set.EqOn (φ₁) (φ₂) s) :
      φ₁ = φ₂

      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)) :
          Subalgebra.toSubmodule (Algebra.adjoin E L) = Submodule.span E 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 : Subalgebra.toSubmodule L = Submodule.span F S) :
          Subalgebra.toSubmodule (Algebra.adjoin E L) = Submodule.span E 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 Subalgebra.adjoin_eq_span_basis {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) {ι : Type u_4} (bL : Basis ι F L) :
          Subalgebra.toSubmodule (Algebra.adjoin E L) = Submodule.span E (Set.range fun (i : ι) => (bL i))

          If K / E / F is a ring extension tower, L is a subalgebra of K / F, then E[L] is generated by any basis of L / F as an E-module.

          theorem Algebra.restrictScalars_adjoin_of_algEquiv {F : Type u_4} {E : Type u_5} {L : Type u_6} {L' : Type u_7} [CommSemiring F] [CommSemiring L] [CommSemiring L'] [Semiring E] [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E] [Algebra F E] [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L') (hi : (algebraMap L E) = (algebraMap L' E) i) (S : Set E) :

          If E / L / F and E / L' / F are two ring extension towers, L ≃ₐ[F] L' is an isomorphism compatible with E / L and E / L', then for any subset S of E, L[S] and L'[S] are equal as subalgebras of E / F.