Mathlib.RingTheory.Adjoin.Tower

Module docstring

{"# Adjoining elements and being finitely generated in an algebra tower

Main results

Algebra.fg_trans': if S is finitely generated as R-algebra and A as S-algebra, then A is finitely generated as R-algebra
fg_of_fg_of_fg: Artin--Tate lemma: if C/B/A is a tower of rings, and A is noetherian, and C is algebra-finite over A, and C is module-finite over B, then B is algebra-finite over A. "}

Algebra.adjoin_restrictScalars theorem

 (C D E : Type*) [CommSemiring C] [CommSemiring D] [CommSemiring E] [Algebra C D] [Algebra C E] [Algebra D E]
  [IsScalarTower C D E] (S : Set E) :
  (Algebra.adjoin D S).restrictScalars C =
    (Algebra.adjoin ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) S).restrictScalars C

Full source

theorem adjoin_restrictScalars (C D E : Type*) [CommSemiring C] [CommSemiring D] [CommSemiring E]
    [Algebra C D] [Algebra C E] [Algebra D E] [IsScalarTower C D E] (S : Set E) :
    (Algebra.adjoin D S).restrictScalars C =
      (Algebra.adjoin ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) S).restrictScalars
        C := by
  suffices
    Set.range (algebraMap D E) =
      Set.range (algebraMap ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) E) by
    ext x
    change x ∈ Subsemiring.closure (_ ∪ S)x ∈ Subsemiring.closure (_ ∪ S) ↔ x ∈ Subsemiring.closure (_ ∪ S)
    rw [this]
  ext x
  constructor
  · rintro ⟨y, hy⟩
    exact ⟨⟨algebraMap D E y, ⟨y, ⟨Algebra.mem_top, rfl⟩⟩⟩, hy⟩
  · rintro ⟨⟨y, ⟨z, ⟨h0, h1⟩⟩⟩, h2⟩
    exact ⟨z, Eq.trans h1 h2⟩

Equality of Restricted Scalar Adjoinments in Algebra Tower

Informal description

Let $C$, $D$, $E$ be commutative semirings with algebra structures $C \to D$, $C \to E$, and $D \to E$ such that these form a scalar tower (i.e., the $C$-action on $E$ factors through $D$). For any subset $S \subseteq E$, the $C$-algebra obtained by restricting scalars from $D$ to $C$ in the $D$-algebra generated by $S$ is equal to the $C$-algebra obtained by restricting scalars from the image of the top $C$-subalgebra of $D$ (under the scalar tower algebra homomorphism) to $C$ in the algebra generated by $S$.

Algebra.adjoin_res_eq_adjoin_res theorem

 (C D E F : Type*) [CommSemiring C] [CommSemiring D] [CommSemiring E] [CommSemiring F] [Algebra C D] [Algebra C E]
  [Algebra C F] [Algebra D F] [Algebra E F] [IsScalarTower C D F] [IsScalarTower C E F] {S : Set D} {T : Set E}
  (hS : Algebra.adjoin C S = ⊤) (hT : Algebra.adjoin C T = ⊤) :
  (Algebra.adjoin E (algebraMap D F '' S)).restrictScalars C =
    (Algebra.adjoin D (algebraMap E F '' T)).restrictScalars C

Full source

theorem adjoin_res_eq_adjoin_res (C D E F : Type*) [CommSemiring C] [CommSemiring D]
    [CommSemiring E] [CommSemiring F] [Algebra C D] [Algebra C E] [Algebra C F] [Algebra D F]
    [Algebra E F] [IsScalarTower C D F] [IsScalarTower C E F] {S : Set D} {T : Set E}
    (hS : Algebra.adjoin C S = ⊤) (hT : Algebra.adjoin C T = ⊤) :
    (Algebra.adjoin E (algebraMapalgebraMap D F '' S)).restrictScalars C =
      (Algebra.adjoin D (algebraMapalgebraMap E F '' T)).restrictScalars C := by
  rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image,
    ← Algebra.adjoin_image, ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom,
    IsScalarTower.coe_toAlgHom, IsScalarTower.coe_toAlgHom, ← adjoin_union_eq_adjoin_adjoin, ←
    adjoin_union_eq_adjoin_adjoin, Set.union_comm]

Equality of Restricted Scalar Adjoinments for Generating Sets in Algebra Tower

Informal description

Let $C$, $D$, $E$, $F$ be commutative semirings with algebra structures $C \to D$, $C \to E$, $C \to F$, $D \to F$, and $E \to F$ forming scalar towers (i.e., the $C$-actions on $F$ factor through $D$ and $E$ respectively). Given subsets $S \subseteq D$ and $T \subseteq E$ such that the $C$-subalgebra generated by $S$ equals the top subalgebra of $D$ and similarly for $T$ in $E$, then the $C$-subalgebras obtained by restricting scalars from $E$ to $C$ in the $E$-subalgebra generated by the image of $S$ under the algebra map $D \to F$ is equal to the $C$-subalgebra obtained by restricting scalars from $D$ to $C$ in the $D$-subalgebra generated by the image of $T$ under the algebra map $E \to F$. In symbols: \[ (\text{adjoin}_E (\text{algebraMap}_{D \to F}(S)))_{\text{restrictScalars } C} = (\text{adjoin}_D (\text{algebraMap}_{E \to F}(T)))_{\text{restrictScalars } C}. \]

Algebra.fg_trans' theorem

 {R S A : Type*} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A]
  [IsScalarTower R S A] (hRS : (⊤ : Subalgebra R S).FG) (hSA : (⊤ : Subalgebra S A).FG) : (⊤ : Subalgebra R A).FG

Full source

theorem Algebra.fg_trans' {R S A : Type*} [CommSemiring R] [CommSemiring S] [Semiring A]
    [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (hRS : (⊤ : Subalgebra R S).FG)
    (hSA : (⊤ : Subalgebra S A).FG) : (⊤ : Subalgebra R A).FG := by
  classical
  rcases hRS with ⟨s, hs⟩
  rcases hSA with ⟨t, ht⟩
  exact ⟨s.image (algebraMap S A) ∪ t, by
    rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
    ⟩

Transitivity of Finite Generation in Algebra Towers

Informal description

Let $R$, $S$, and $A$ be commutative semirings with algebra structures $R \to S$, $S \to A$, and $R \to A$ forming a scalar tower (i.e., the $R$-action on $A$ factors through $S$). If the $R$-algebra $S$ is finitely generated and the $S$-algebra $A$ is finitely generated, then the $R$-algebra $A$ is finitely generated.

exists_subalgebra_of_fg theorem

 (hAC : (⊤ : Subalgebra A C).FG) (hBC : (⊤ : Submodule B C).FG) : ∃ B₀ : Subalgebra A B, B₀.FG ∧ (⊤ : Submodule B₀ C).FG

Full source

theorem exists_subalgebra_of_fg (hAC : (⊤ : Subalgebra A C).FG) (hBC : (⊤ : Submodule B C).FG) :
    ∃ B₀ : Subalgebra A B, B₀.FG ∧ (⊤ : Submodule B₀ C).FG := by
  obtain ⟨x, hx⟩ := hAC
  obtain ⟨y, hy⟩ := hBC
  have := hy
  simp_rw [eq_top_iff', mem_span_finset] at this
  choose f _ hf using this
  classical
  let s : Finset B := Finset.image₂ f (x ∪ y * y) y
  have hxy :
    ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
    fun xi hxi =>
    hf xi ▸
      sum_mem fun yj hyj =>
        smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
          ⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
          (subset_span <| mem_insert_of_mem hyj)
  have hyy :
    span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
        span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
      span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := by
    rw [span_mul_span, span_le, coe_insert]
    rintro _ ⟨yi, rfl | hyi, yj, rfl | hyj, rfl⟩ <;> dsimp
    · rw [mul_one]
      exact subset_span (Set.mem_insert _ _)
    · rw [one_mul]
      exact subset_span (Set.mem_insert_of_mem _ hyj)
    · rw [mul_one]
      exact subset_span (Set.mem_insert_of_mem _ hyi)
    · rw [← hf (yi * yj)]
      exact
        SetLike.mem_coe.2
          (sum_mem fun yk hyk =>
            smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
              ⟨f (yi * yj) yk,
                Algebra.subset_adjoin <|
                  mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
              (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
  refine ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, ?_⟩
  convert restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _
  rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span,
    span_le]
  refine fun r hr =>
    Submonoid.closure_induction (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _)
      (fun p q _ _ hp hq => hyy <| Submodule.mul_mem_mul hp hq) hr

Existence of Finitely Generated Intermediate Subalgebra in Tower of Algebras

Informal description

Let $A \subseteq B \subseteq C$ be a tower of commutative rings. If $C$ is finitely generated as an $A$-algebra and $C$ is finitely generated as a $B$-module, then there exists a finitely generated $A$-subalgebra $B_0$ of $B$ such that $C$ is finitely generated as a $B_0$-module.

fg_of_fg_of_fg theorem

 [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).FG) (hBC : (⊤ : Submodule B C).FG)
  (hBCi : Function.Injective (algebraMap B C)) : (⊤ : Subalgebra A B).FG

Full source

/-- **Artin--Tate lemma**: if A ⊆ B ⊆ C is a chain of subrings of commutative rings, and
A is noetherian, and C is algebra-finite over A, and C is module-finite over B,
then B is algebra-finite over A.

References: Atiyah--Macdonald Proposition 7.8; Altman--Kleiman 16.17. -/
@[stacks 00IS]
theorem fg_of_fg_of_fg [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).FG)
    (hBC : (⊤ : Submodule B C).FG) (hBCi : Function.Injective (algebraMap B C)) :
    (⊤ : Subalgebra A B).FG :=
  let ⟨B₀, hAB₀, hB₀C⟩ := exists_subalgebra_of_fg A B C hAC hBC
  Algebra.fg_trans' (B₀.fg_top.2 hAB₀) <|
    Subalgebra.fg_of_submodule_fg <|
      have : IsNoetherianRing B₀ := isNoetherianRing_of_fg hAB₀
      have : Module.Finite B₀ C := ⟨hB₀C⟩
      fg_of_injective (IsScalarTower.toAlgHom B₀ B C).toLinearMap hBCi

Artin--Tate Lemma: Finiteness of Intermediate Algebra in Tower

Informal description

Let $A \subseteq B \subseteq C$ be a tower of commutative rings, where $A$ is noetherian. If $C$ is finitely generated as an $A$-algebra, $C$ is finitely generated as a $B$-module, and the algebra map $B \to C$ is injective, then $B$ is finitely generated as an $A$-algebra.