Adjoining elements to form subalgebras

This file contains basic results on Algebra.adjoin.

Tags

adjoin, algebra

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) : adjoin R (s ×ˢ t) ≤ (adjoin R s).prod (adjoin R t)

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) : adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1})) = (adjoin R s).prod (adjoin R t)

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) : adjoin R (⇑(algebraMap S A) '' s) = Subalgebra.map (IsScalarTower.toAlgHom R S A) (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) : adjoin R (⇑(algebraMap S A) '' s ∪ t) = Subalgebra.restrictScalars R (adjoin (↥(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) : adjoin S ↑(adjoin R s) = adjoin S s

theorem Algebra.Subalgebra.restrictScalars_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 A} : Subalgebra.restrictScalars R (adjoin S s) = (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R s

@[simp]

theorem Algebra.adjoin_top (R : Type uR) {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] {A : Type u_1} [Semiring A] [Algebra S A] (t : Set A) : adjoin (↥⊤) t = Subalgebra.restrictScalars (↥⊤) (adjoin S t)

theorem Algebra.adjoin_union_eq_adjoin_adjoin (R : Type uR) {A : Type uA} [CommSemiring R] [CommSemiring A] [Algebra R A] (s t : Set A) : adjoin R (s ∪ t) = Subalgebra.restrictScalars R (adjoin (↥(adjoin R s)) 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 ∈ adjoin R s) (hr : (algebraMap A B) r ∈ B') : ∃ (n₀ : ℕ), ∀ n ≥ n₀, 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 ∈ adjoin R s) : ∃ (n₀ : ℕ), ∀ n ≥ n₀, r ^ n • x ∈ adjoin R (r • s)

theorem Algebra.adjoin_nonUnitalSubalgebra_eq_span {R : Type uR} {A : Type uA} [CommSemiring R] [CommSemiring A] [Algebra R A] (s : NonUnitalSubalgebra R A) : Subalgebra.toSubmodule (adjoin R ↑s) = Submodule.span R {1} ⊔ s.toSubmodule

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) : 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 (F : Type u_4) [CommSemiring F] {E : Type u_5} [CommSemiring E] [Algebra F E] (K : Subalgebra F E) (S : Set E) : Subalgebra.restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)

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) : Subalgebra.restrictScalars F (adjoin L S) = Subalgebra.restrictScalars F (adjoin L' S)

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.