Mathlib.RingTheory.Adjoin.Basic

Algebra.adjoin_prod_le theorem

(s : Set A) (t : Set B) : adjoin R (s ×ˢ t) ≤ (adjoin R s).prod (adjoin R t)

Full source

theorem adjoin_prod_le (s : Set A) (t : Set B) :
    adjoin R (s ×ˢ t) ≤ (adjoin R s).prod (adjoin R t) :=
  adjoin_le <| Set.prod_mono subset_adjoin subset_adjoin

Subalgebra Generated by Product is Contained in Product of Subalgebras

Informal description

Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. For any subsets $s \subseteq A$ and $t \subseteq B$, the $R$-subalgebra generated by the Cartesian product $s \times t$ is contained in the product of the $R$-subalgebra generated by $s$ and the $R$-subalgebra generated by $t$.

Algebra.adjoin_inl_union_inr_eq_prod theorem

 (s) (t) :
  adjoin R (LinearMap.inl R A B '' (s ∪ { 1 }) ∪ LinearMap.inr R A B '' (t ∪ { 1 })) = (adjoin R s).prod (adjoin R t)

Full source

theorem adjoin_inl_union_inr_eq_prod (s) (t) :
    adjoin R (LinearMap.inlLinearMap.inl R A B '' (s ∪ {1})LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1})) =
      (adjoin R s).prod (adjoin R t) := by
  apply le_antisymm
  · simp only [adjoin_le_iff, Set.insert_subset_iff, Subalgebra.zero_mem, Subalgebra.one_mem,
      subset_adjoin,-- the rest comes from `squeeze_simp`
      Set.union_subset_iff,
      LinearMap.coe_inl, Set.mk_preimage_prod_right, Set.image_subset_iff, SetLike.mem_coe,
      Set.mk_preimage_prod_left, LinearMap.coe_inr, and_self_iff, Set.union_singleton,
      Subalgebra.coe_prod]
  · rintro ⟨a, b⟩ ⟨ha, hb⟩
    let P := adjoin R (LinearMap.inlLinearMap.inl R A B '' (s ∪ {1})LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1}))
    have Ha : (a, (0 : B))(a, (0 : B)) ∈ adjoin R (LinearMap.inl R A B '' (s ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inl_map_mul ha
    have Hb : ((0 : A), b)((0 : A), b) ∈ adjoin R (LinearMap.inr R A B '' (t ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inr_map_mul hb
    replace Ha : (a, (0 : B))(a, (0 : B)) ∈ P := adjoin_mono Set.subset_union_left Ha
    replace Hb : ((0 : A), b)((0 : A), b) ∈ P := adjoin_mono Set.subset_union_right Hb
    simpa [P] using Subalgebra.add_mem _ Ha Hb

Adjoint of Union of Injected Sets Equals Product of Adjoints

Informal description

Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. For any subsets $s \subseteq A$ and $t \subseteq B$, the $R$-subalgebra generated by the union of: 1. The image of $s \cup \{1\}$ under the left injection linear map $\text{inl} : A \to A \times B$, and 2. The image of $t \cup \{1\}$ under the right injection linear map $\text{inr} : B \to A \times B$ is equal to the product of the $R$-subalgebras generated by $s$ in $A$ and by $t$ in $B$, i.e., \[ \text{adjoin}_R(\text{inl}(s \cup \{1\}) \cup \text{inr}(t \cup \{1\})) = (\text{adjoin}_R s) \times (\text{adjoin}_R t). \]

Algebra.adjoin_algebraMap theorem

(s : Set S) : adjoin R (algebraMap S A '' s) = (adjoin R s).map (IsScalarTower.toAlgHom R S A)

Full source

theorem adjoin_algebraMap (s : Set S) :
    adjoin R (algebraMapalgebraMap S A '' s) = (adjoin R s).map (IsScalarTower.toAlgHom R S A) :=
  adjoin_image R (IsScalarTower.toAlgHom R S A) s

Adjoint of algebra map equals image of adjoint under scalar tower homomorphism

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra, and $A$ an $S$-algebra. For any subset $s \subseteq S$, the $R$-subalgebra generated by the image of $s$ under the algebra map $S \to A$ is equal to the image of the $R$-subalgebra generated by $s$ under the canonical algebra homomorphism $S \to A$ induced by the scalar tower structure.

Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin theorem

(s : Set S) (t : Set A) : adjoin R (algebraMap S A '' s ∪ t) = (adjoin (adjoin R s) t).restrictScalars R

Full source

theorem adjoin_algebraMap_image_union_eq_adjoin_adjoin (s : Set S) (t : Set A) :
    adjoin R (algebraMapalgebraMap S A '' salgebraMap S A '' s ∪ t) = (adjoin (adjoin R s) t).restrictScalars R :=
  le_antisymm
    (closure_mono <|
      Set.union_subset (Set.range_subset_iff.2 fun r => Or.inl ⟨algebraMap R (adjoin R s) r,
        (IsScalarTower.algebraMap_apply _ _ _ _).symm⟩)
        (Set.union_subset_union_left _ fun _ ⟨_x, hx, hxs⟩ => hxs ▸ ⟨⟨_, subset_adjoin hx⟩, rfl⟩))
    (closure_le.2 <|
      Set.union_subset (Set.range_subset_iff.2 fun x => adjoin_mono Set.subset_union_left <|
        Algebra.adjoin_algebraMap R A s ▸ ⟨x, x.prop, rfl⟩)
        (Set.Subset.trans Set.subset_union_right subset_adjoin))

Adjoint of Union of Algebra Map Image and Set Equals Restricted Scalar Adjoint

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra, and $A$ an $S$-algebra. For any subsets $s \subseteq S$ and $t \subseteq A$, the $R$-subalgebra generated by the union of the image of $s$ under the algebra map $S \to A$ and the set $t$ is equal to the $R$-subalgebra obtained by restricting scalars of the $S$-subalgebra generated by $t$ over the $R$-subalgebra generated by $s$. In symbols: \[ \text{adjoin}_R(\text{algebraMap}_{S \to A}(s) \cup t) = (\text{adjoin}_{\text{adjoin}_R s} t)_{\text{restrictScalars } R}. \]

Algebra.adjoin_adjoin_of_tower theorem

(s : Set A) : adjoin S (adjoin R s : Set A) = adjoin S s

Full source

theorem adjoin_adjoin_of_tower (s : Set A) : adjoin S (adjoin R s : Set A) = adjoin S s := by
  apply le_antisymm (adjoin_le _)
  · exact adjoin_mono subset_adjoin
  · change adjoin R s ≤ (adjoin S s).restrictScalars R
    refine adjoin_le ?_
    -- Porting note: unclear why this was broken
    have : (Subalgebra.restrictScalars R (adjoin S s) : Set A) = adjoin S s := rfl
    rw [this]
    exact subset_adjoin

Tower Property of Algebra Adjoints: $\text{adjoin}_S(\text{adjoin}_R(s)) = \text{adjoin}_S(s)$

Informal description

Let $R \subseteq S \subseteq A$ be a tower of algebras. For any subset $s \subseteq A$, the $S$-subalgebra generated by the $R$-subalgebra generated by $s$ is equal to the $S$-subalgebra generated by $s$ itself. In other words, $\text{adjoin}_S(\text{adjoin}_R(s)) = \text{adjoin}_S(s)$.

Algebra.Subalgebra.restrictScalars_adjoin theorem

{s : Set A} : (adjoin S s).restrictScalars R = (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R s

Full source

theorem Subalgebra.restrictScalars_adjoin {s : Set A} :
    (adjoin S s).restrictScalars R = (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R s := by
  refine le_antisymm (fun _ hx ↦ adjoin_induction
    (fun x hx ↦ le_sup_right (α := Subalgebra R A) (subset_adjoin hx))
    (fun x ↦ le_sup_left (α := Subalgebra R A) ⟨x, rfl⟩)
    (fun _ _ _ _ ↦ add_mem) (fun _ _ _ _ ↦ mul_mem) <|
    (Subalgebra.mem_restrictScalars _).mp hx) (sup_le ?_ <| adjoin_le subset_adjoin)
  rintro _ ⟨x, rfl⟩; exact algebraMap_mem (adjoin S s) x

Restriction of Adjoined Subalgebra Equals Supremum of Range and Adjoined Subalgebra

Informal description

For any subset $s$ of an algebra $A$ over a commutative ring $R$ and a commutative ring $S$ with $R \subseteq S \subseteq A$, the subalgebra generated by $s$ over $S$ restricted to scalars in $R$ is equal to the supremum of the image of the algebra homomorphism from $S$ to $A$ and the subalgebra generated by $s$ over $R$. In symbols: $$(\text{adjoin}_S s)_{\text{restrictScalars } R} = \text{range}(\text{IsScalarTower.toAlgHom } R S A) \sqcup \text{adjoin}_R s.$$

Algebra.adjoin_top theorem

 {A} [Semiring A] [Algebra S A] (t : Set A) :
  adjoin (⊤ : Subalgebra R S) t = (adjoin S t).restrictScalars (⊤ : Subalgebra R S)

Full source

@[simp]
theorem adjoin_top {A} [Semiring A] [Algebra S A] (t : Set A) :
    adjoin (⊤ : Subalgebra R S) t = (adjoin S t).restrictScalars (⊤ : Subalgebra R S) :=
  let equivTop : SubalgebraSubalgebra (⊤ : Subalgebra R S) A ≃o Subalgebra S A :=
    { toFun := fun s => { s with algebraMap_mem' := fun r => s.algebraMap_mem ⟨r, trivial⟩ }
      invFun := fun s => s.restrictScalars _
      left_inv := fun _ => SetLike.coe_injective rfl
      right_inv := fun _ => SetLike.coe_injective rfl
      map_rel_iff' := @fun _ _ => Iff.rfl }
  le_antisymm
    (adjoin_le <| show t ⊆ adjoin S t from subset_adjoin)
    (equivTop.symm_apply_le.mpr <|
      adjoin_le <| show t ⊆ adjoin (⊤ : Subalgebra R S) t from subset_adjoin)

Adjoint of Top Subalgebra Equals Restricted Scalar Adjoint

Informal description

Let $A$ be a semiring with an algebra structure over $S$, and let $t$ be a subset of $A$. Then the subalgebra generated by $t$ over the top subalgebra of $S$ (viewed as an algebra over $R$) is equal to the subalgebra generated by $t$ over $S$, restricted to scalars in the top subalgebra of $S$ over $R$.

Algebra.adjoin_union_eq_adjoin_adjoin theorem

: adjoin R (s ∪ t) = (adjoin (adjoin R s) t).restrictScalars R

Full source

theorem adjoin_union_eq_adjoin_adjoin :
    adjoin R (s ∪ t) = (adjoin (adjoin R s) t).restrictScalars R := by
  simpa using adjoin_algebraMap_image_union_eq_adjoin_adjoin R s t

Adjoint of Union Equals Restricted Scalar Adjoint of Adjoints

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any subsets $s, t \subseteq A$, the $R$-subalgebra generated by the union $s \cup t$ is equal to the $R$-subalgebra obtained by restricting scalars of the subalgebra generated by $t$ over the subalgebra generated by $s$. In symbols: \[ \text{adjoin}_R(s \cup t) = (\text{adjoin}_{\text{adjoin}_R s} t)_{\text{restrictScalars } R}. \]

Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin theorem

 [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'

Full source

theorem pow_smul_mem_of_smul_subset_of_mem_adjoin [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 : algebraMapalgebraMap A B r ∈ B') : ∃ n₀ : ℕ, ∀ n ≥ n₀, r ^ n • x ∈ B' := by
  change x ∈ Subalgebra.toSubmodule (adjoin R s) at hx
  rw [adjoin_eq_span, Finsupp.mem_span_iff_linearCombination] at hx
  rcases hx with ⟨l, rfl : (l.sum fun (i : Submonoid.closure s) (c : R) => c • (i : B)) = x⟩
  choose n₁ n₂ using fun x : Submonoid.closure s => Submonoid.pow_smul_mem_closure_smul r s x.prop
  use l.support.sup n₁
  intro n hn
  rw [Finsupp.smul_sum]
  refine B'.toSubmodule.sum_mem ?_
  intro a ha
  have : n ≥ n₁ a := le_trans (Finset.le_sup ha) hn
  dsimp only
  rw [← tsub_add_cancel_of_le this, pow_add, ← smul_smul, ←
    IsScalarTower.algebraMap_smul A (l a) (a : B), smul_smul (r ^ n₁ a), mul_comm, ← smul_smul,
    smul_def, map_pow, IsScalarTower.algebraMap_smul]
  apply Subalgebra.mul_mem _ (Subalgebra.pow_mem _ hr _) _
  refine Subalgebra.smul_mem _ ?_ _
  change _ ∈ B'.toSubmonoid
  rw [← Submonoid.closure_eq B'.toSubmonoid]
  apply Submonoid.closure_mono hs (n₂ a)

Existence of Power Scalar Multiple in Subalgebra under Scalar Action Condition

Informal description

Let $R$, $A$, and $B$ be commutative semirings with $B$ equipped with algebra structures over both $R$ and $A$, such that $R \to A \to B$ forms a scalar tower. Given an element $r \in A$, a subset $s \subseteq B$, and a subalgebra $B'$ of $B$ over $R$ such that $r \cdot s \subseteq B'$, if $x \in B$ is in the subalgebra generated by $s$ over $R$ and the image of $r$ under the algebra map $A \to B$ lies in $B'$, then there exists a natural number $n_0$ such that for all $n \geq n_0$, the element $r^n \cdot x$ is in $B'$.

Algebra.pow_smul_mem_adjoin_smul theorem

 (r : R) (s : Set A) {x : A} (hx : x ∈ adjoin R s) : ∃ n₀ : ℕ, ∀ n ≥ n₀, r ^ n • x ∈ adjoin R (r • s)

Full source

theorem pow_smul_mem_adjoin_smul (r : R) (s : Set A) {x : A} (hx : x ∈ adjoin R s) :
    ∃ n₀ : ℕ, ∀ n ≥ n₀, r ^ n • x ∈ adjoin R (r • s) :=
  pow_smul_mem_of_smul_subset_of_mem_adjoin r s _ subset_adjoin hx (Subalgebra.algebraMap_mem _ _)

Existence of Power Scalar Multiple in Adjoined Subalgebra under Scalar Action

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any element $r \in R$ and subset $s \subseteq A$, if $x \in A$ is in the subalgebra generated by $s$ over $R$, then there exists a natural number $n_0$ such that for all $n \geq n_0$, the element $r^n \cdot x$ is in the subalgebra generated by $r \cdot s$ over $R$.

Algebra.adjoin_nonUnitalSubalgebra_eq_span theorem

(s : NonUnitalSubalgebra R A) : Subalgebra.toSubmodule (adjoin R (s : Set A)) = span R { 1 } ⊔ s.toSubmodule

Full source

lemma adjoin_nonUnitalSubalgebra_eq_span (s : NonUnitalSubalgebra R A) :
    Subalgebra.toSubmodule (adjoin R (s : Set A)) = spanspan R {1} ⊔ s.toSubmodule := by
  rw [adjoin_eq_span, Submonoid.closure_eq_one_union, span_union, ← NonUnitalAlgebra.adjoin_eq_span,
      NonUnitalAlgebra.adjoin_eq]

Adjoined Non-Unital Subalgebra as Span of Identity and Submodule

Informal description

For any non-unital subalgebra $s$ of an algebra $A$ over a commutative semiring $R$, the submodule generated by the subalgebra obtained by adjoining $s$ to $R$ is equal to the span of the singleton set $\{1\}$ joined with the submodule corresponding to $s$. That is, \[ \text{Subalgebra.toSubmodule}(\text{adjoin}_R(s)) = \text{span}_R(\{1\}) \sqcup s.\text{toSubmodule}. \]

Subalgebra.adjoin_eq_span_basis theorem

{ι : Type*} (bL : Basis ι F L) : toSubmodule (adjoin E (L : Set K)) = span E (Set.range fun i : ι ↦ (bL i).1)

Full source

/-- 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 Subalgebra.adjoin_eq_span_basis {ι : Type*} (bL : Basis ι F L) :
    toSubmodule (adjoin E (L : Set K)) = span E (Set.range fun i : ι ↦ (bL i).1) :=
  L.adjoin_eq_span_of_eq_span E <| by
    simpa only [← L.range_val, Submodule.map_span, Submodule.map_top, ← Set.range_comp]
      using congr_arg (Submodule.map L.val) bL.span_eq.symm

Adjoined Subalgebra as Span of Basis Vectors in Extension Tower

Informal description

Let $K/E/F$ be a tower of ring extensions, and let $L$ be a subalgebra of $K$ over $F$. Given a basis $b_L$ of $L$ over $F$ indexed by $\iota$, the submodule corresponding to the subalgebra $E[L]$ (obtained by adjoining $L$ to $E$ in $K$) is equal to the $E$-linear span of the basis vectors $\{b_L(i) \mid i \in \iota\}$.

Algebra.restrictScalars_adjoin theorem

 (F : Type*) [CommSemiring F] {E : Type*} [CommSemiring E] [Algebra F E] (K : Subalgebra F E) (S : Set E) :
  (Algebra.adjoin K S).restrictScalars F = Algebra.adjoin F (K ∪ S)

Full source

theorem Algebra.restrictScalars_adjoin (F : Type*) [CommSemiring F] {E : Type*} [CommSemiring E]
    [Algebra F E] (K : Subalgebra F E) (S : Set E) :
    (Algebra.adjoin K S).restrictScalars F = Algebra.adjoin F (K ∪ S) := by
  conv_lhs => rw [← Algebra.adjoin_eq K, ← Algebra.adjoin_union_eq_adjoin_adjoin]

Equality of Restricted Scalar Adjoint and Union Adjoint in Algebra

Informal description

Let $F$ be a commutative semiring, $E$ a commutative semiring with an $F$-algebra structure, and $K$ a subalgebra of $E$ over $F$. For any subset $S \subseteq E$, the subalgebra generated by $S$ over $K$ (with scalars restricted back to $F$) is equal to the subalgebra generated by $K \cup S$ over $F$. In symbols: \[ (\text{adjoin}_K S)_{\text{restrictScalars } F} = \text{adjoin}_F (K \cup S). \]

Algebra.restrictScalars_adjoin_of_algEquiv theorem

 {F E L L' : Type*} [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) :
  (Algebra.adjoin L S).restrictScalars F = (Algebra.adjoin L' S).restrictScalars F

Full source

/-- 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`. -/
theorem Algebra.restrictScalars_adjoin_of_algEquiv
    {F E L L' : Type*} [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) :
    (Algebra.adjoin L S).restrictScalars F = (Algebra.adjoin L' S).restrictScalars F := by
  apply_fun Subalgebra.toSubsemiring using fun K K' h ↦ by rwa [SetLike.ext'_iff] at h ⊢
  change Subsemiring.closure _ = Subsemiring.closure _
  rw [hi, Set.range_comp, EquivLike.range_eq_univ, Set.image_univ]

Equality of Adjoined Subalgebras under Compatible Algebra Isomorphism

Informal description

Let $F$, $E$, $L$, and $L'$ be commutative semirings with $L$ and $L'$ being $F$-algebras, and $E$ an $L$-algebra and $L'$-algebra such that $E$ is also an $F$-algebra with compatible scalar towers $F \subseteq L \subseteq E$ and $F \subseteq L' \subseteq E$. Given an $F$-algebra isomorphism $i: L \simeq L'$ satisfying $\text{algebraMap}_L^E = \text{algebraMap}_{L'}^E \circ i$, then for any subset $S \subseteq E$, the subalgebras $\text{adjoin}_L(S)$ and $\text{adjoin}_{L'}(S)$ are equal when restricted to scalars in $F$.

Tags