chore(RingTheory): reorganize imports around locality properties of finiteness (leanprover-community#36044)

Author: chrisflav

Mathlib.lean

@@ -6134,6 +6134,8 @@ public import Mathlib.RingTheory.Finiteness.Cardinality
 public import Mathlib.RingTheory.Finiteness.Cofinite
 public import Mathlib.RingTheory.Finiteness.Defs
 public import Mathlib.RingTheory.Finiteness.Descent
+public import Mathlib.RingTheory.Finiteness.FinitePresentationLocal
+public import Mathlib.RingTheory.Finiteness.FiniteTypeLocal
 public import Mathlib.RingTheory.Finiteness.Finsupp
 public import Mathlib.RingTheory.Finiteness.Ideal
 public import Mathlib.RingTheory.Finiteness.Lattice

Mathlib/RingTheory/Finiteness/FinitePresentationLocal.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2024 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+module
+
+public import Mathlib.RingTheory.Finiteness.FiniteTypeLocal
+public import Mathlib.RingTheory.Localization.Away.AdjoinRoot
+
+/-!
+
+# `Algebra.FinitePresentation` is local
+
+In this file we show that being a finitely presented algebra is local.
+
+## Main results
+
+- `Algebra.FinitePresentation.of_span_eq_top_target`: finite presentation is local on the
+  (algebraic) target
+
+-/
+
+@[expose] public section
+
+open scoped Pointwise TensorProduct
+
+namespace Algebra.FinitePresentation
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
+
+/--
+If `S` is an `R`-algebra with a surjection from a finitely-presented `R`-algebra `A`, such that
+localized at a spanning set `{ r }` of elements of `A`, `Sᵣ` is finitely-presented, then
+`S` is finitely presented.
+This is almost `finitePresentation_ofLocalizationSpanTarget`. The difference is,
+that here the set `t` generates the unit ideal of `A`, while in the general version,
+it only generates a quotient of `A`.
+-/
+lemma of_span_eq_top_target_aux {A : Type*} [CommRing A] [Algebra R A]
+    [Algebra.FinitePresentation R A] (f : A →ₐ[R] S) (hf : Function.Surjective f)
+    (t : Finset A) (ht : Ideal.span (t : Set A) = ⊤)
+    (H : ∀ g : t, Algebra.FinitePresentation R (Localization.Away (f g))) :
+    Algebra.FinitePresentation R S := by
+  apply Algebra.FinitePresentation.of_surjective hf
+  apply RingHom.ker_fg_of_localizationSpan t ht
+  intro g
+  let f' : Localization.Away g.val →ₐ[R] Localization.Away (f g) :=
+    Localization.awayMapₐ f g.val
+  have (g : t) : Algebra.FinitePresentation R (Localization.Away g.val) :=
+    haveI : Algebra.FinitePresentation A (Localization.Away g.val) :=
+      IsLocalization.Away.finitePresentation g.val
+    Algebra.FinitePresentation.trans R A (Localization.Away g.val)
+  apply Algebra.FinitePresentation.ker_fG_of_surjective f'
+  exact IsLocalization.Away.mapₐ_surjective_of_surjective _ hf
+
+universe u
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Finite-presentation can be checked on a standard covering of the target. -/
+lemma of_span_eq_top_target (s : Set S) (hs : Ideal.span (s : Set S) = ⊤)
+    (h : ∀ i ∈ s, Algebra.FinitePresentation R (Localization.Away i)) :
+    Algebra.FinitePresentation R S := by
+  obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
+  replace h (i : s) : Algebra.FinitePresentation R (Localization.Away i.val) := h i (h₁ i.property)
+  classical
+  /-
+  We already know that `S` is of finite type over `R`, so we have a surjection
+  `MvPolynomial (Fin n) R →ₐ[R] S`. To reason about the kernel, we want to check it on the stalks
+  of preimages of `s`. But the preimages do not necessarily span `MvPolynomial (Fin n) R`, so
+  we quotient out by an ideal and apply `finitePresentation_ofLocalizationSpanTarget_aux`.
+  -/
+  have hfintype : Algebra.FiniteType R S := by
+    apply Algebra.FiniteType.of_span_eq_top_target s hs
+    intro x hx
+    have := h ⟨x, hx⟩
+    infer_instance
+  obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp hfintype
+  obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_linearCombination S (s : Set S) 1).mp
+      (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
+  choose g' hg' using (fun g : s ↦ hf g)
+  choose h' hh' using (fun g : s ↦ hf (l g))
+  let I : Ideal (MvPolynomial (Fin n) R) := Ideal.span { ∑ g : s, g' g * h' g - 1 }
+  let A := MvPolynomial (Fin n) R ⧸ I
+  have hfI : ∀ a ∈ I, f a = 0 := by
+    intro p hp
+    simp only [Finset.univ_eq_attach, I, Ideal.mem_span_singleton] at hp
+    obtain ⟨q, rfl⟩ := hp
+    simp only [map_mul, map_sub, map_sum, map_one, hg', hh']
+    rw [Finsupp.linearCombination_apply_of_mem_supported (α := (s : Set S)) S (s := s.attach)] at hl
+    · rw [← hl]
+      simp only [Finset.coe_sort_coe, smul_eq_mul, mul_comm, sub_self, zero_mul]
+    · rintro a -
+      simp
+  let f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
+  have hf' : Function.Surjective f' :=
+    Ideal.Quotient.lift_surjective_of_surjective I hfI hf
+  let t : Finset A := Finset.image (fun g ↦ g' g) Finset.univ
+  have ht : Ideal.span (t : Set A) = ⊤ := by
+    rw [Ideal.eq_top_iff_one]
+    have : ∑ g : { x // x ∈ s }, g' g * h' g = (1 : A) := by
+      apply eq_of_sub_eq_zero
+      rw [← map_one (Ideal.Quotient.mk I), ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
+      apply Ideal.subset_span
+      simp
+    simp_rw [← this, Finset.univ_eq_attach, map_sum, map_mul]
+    refine Ideal.sum_mem _ (fun g _ ↦ Ideal.mul_mem_right _ _ <| Ideal.subset_span ?_)
+    simp [t]
+  have : Algebra.FinitePresentation R A := by
+    apply Algebra.FinitePresentation.quotient
+    simp only [Finset.univ_eq_attach, I]
+    exact ⟨{∑ g ∈ s.attach, g' g * h' g - 1}, by simp⟩
+  have Ht (g : t) : Algebra.FinitePresentation R (Localization.Away (f' g)) := by
+    have : ∃ (a : S) (hb : a ∈ s), (Ideal.Quotient.mk I) (g' ⟨a, hb⟩) = g.val := by
+      obtain ⟨g, hg⟩ := g
+      convert hg
+      simp [A, t]
+    obtain ⟨r, hr, hrr⟩ := this
+    simp only [f']
+    rw [← hrr, Ideal.Quotient.liftₐ_apply, Ideal.Quotient.lift_mk]
+    simp_rw +instances [RingHom.coe_coe]
+    rw [hg']
+    apply h
+  exact of_span_eq_top_target_aux f' hf' t ht Ht
+
+/-- Finite-presentation can be checked on a standard covering of the target. -/
+lemma of_span_eq_top_target_of_isLocalizationAway {ι : Type*} (s : ι → S)
+    (hs : Ideal.span (Set.range s) = ⊤) (T : ι → Type*) [∀ i, CommRing (T i)] [∀ i, Algebra R (T i)]
+    [∀ i, Algebra S (T i)] [∀ i, IsScalarTower R S (T i)] [∀ i, IsLocalization.Away (s i) (T i)]
+    [∀ i, Algebra.FinitePresentation R (T i)] :
+    Algebra.FinitePresentation R S := by
+  apply of_span_eq_top_target _ hs
+  rintro - ⟨i, rfl⟩
+  exact .equiv <| (IsLocalization.algEquiv (.powers <| s i) _ (T i)).symm |>.restrictScalars R
+
+instance pi {ι : Type*} [Finite ι] (S : ι → Type*) [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)]
+    [∀ i, Algebra.FinitePresentation R (S i)] :
+    Algebra.FinitePresentation R (∀ a, S a) := by
+  classical
+  let (i : ι) : Algebra (Π a, S a) (S i) := (Pi.evalAlgHom R S i).toAlgebra
+  have (i : ι) : IsLocalization.Away (Pi.single i 1 : ∀ a, S a) (S i) := by
+    refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
+      ((Pi.evalRingHom S i).surjective)
+    simp [IsIdempotentElem, ← Pi.single_mul_left]
+  exact Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
+    _ (Ideal.span_single_eq_top S) (fun i ↦ S i)
+
+end Algebra.FinitePresentation

Mathlib/RingTheory/Finiteness/FiniteTypeLocal.lean

@@ -0,0 +1,166 @@
+/-
+Copyright (c) 2021 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+module
+
+public import Mathlib.RingTheory.FiniteType
+public import Mathlib.RingTheory.Localization.Finiteness
+public import Mathlib.RingTheory.Localization.BaseChange
+
+/-!
+
+# Locality of `Algebra.FiniteType`
+
+In this file we show that finite-type is local on the source and the target.
+
+## Main results
+
+- `Algebra.FiniteType.of_span_eq_top_source`: finite-type is local on the (algebraic) source
+- `Algebra.FiniteType.of_span_eq_top_target`: finite-type is local on the (algebraic) target
+
+-/
+
+public section
+
+section Algebra
+
+open scoped Pointwise TensorProduct
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] (M : Submonoid R)
+variable (R' S' : Type*) [CommRing R'] [CommRing S']
+variable [Algebra R R'] [Algebra S S']
+
+variable {S'} in
+open scoped Classical in
+/-- Let `S` be an `R`-algebra, `M` a submonoid of `S`, `S' = M⁻¹S`.
+Suppose the image of some `x : S` falls in the adjoin of some finite `s ⊆ S'` over `R`,
+and `A` is an `R`-subalgebra of `S` containing both `M` and the numerators of `s`.
+Then, there exists some `m : M` such that `m • x` falls in `A`.
+-/
+theorem IsLocalization.exists_smul_mem_of_mem_adjoin [Algebra R S']
+    [IsScalarTower R S S'] (M : Submonoid S) [IsLocalization M S'] (x : S) (s : Finset S')
+    (A : Subalgebra R S) (hA₁ : (IsLocalization.finsetIntegerMultiple M s : Set S) ⊆ A)
+    (hA₂ : M ≤ A.toSubmonoid) (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) :
+    ∃ m : M, m • x ∈ A := by
+  let g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
+  let y := IsLocalization.commonDenomOfFinset M s
+  have hx₁ : (y : S) • (s : Set S') = g '' _ :=
+    (IsLocalization.finsetIntegerMultiple_image _ s).symm
+  obtain ⟨n, hn⟩ :=
+    Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin (y : S) (s : Set S') (A.map g)
+      (by rw [hx₁]; exact Set.image_mono hA₁) hx (Set.mem_image_of_mem _ (hA₂ y.2))
+  obtain ⟨x', hx', hx''⟩ := hn n (le_of_eq rfl)
+  rw [Algebra.smul_def, ← map_mul] at hx''
+  obtain ⟨a, ha₂⟩ := (IsLocalization.eq_iff_exists M S').mp hx''
+  use a * y ^ n
+  convert A.mul_mem hx' (hA₂ a.prop) using 1
+  rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂,
+    mul_comm]
+
+variable {S'} in
+open scoped Classical in
+/-- Let `S` be an `R`-algebra, `M` a submonoid of `R`, and `S' = M⁻¹S`.
+If the image of some `x : S` falls in the adjoin of some finite `s ⊆ S'` over `R`,
+then there exists some `m : M` such that `m • x` falls in the
+adjoin of `IsLocalization.finsetIntegerMultiple _ s` over `R`.
+-/
+theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple [Algebra R S']
+    [IsScalarTower R S S'] [IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S')
+    (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) :
+    ∃ m : M, m • x ∈
+      Algebra.adjoin R
+        (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S) := by
+  obtain ⟨⟨_, a, ha, rfl⟩, e⟩ :=
+    IsLocalization.exists_smul_mem_of_mem_adjoin (M.map (algebraMap R S)) x s (Algebra.adjoin R _)
+      Algebra.subset_adjoin (by rintro _ ⟨a, _, rfl⟩; exact Subalgebra.algebraMap_mem _ a) hx
+  refine ⟨⟨a, ha⟩, ?_⟩
+  simpa only [Submonoid.smul_def, algebraMap_smul] using e
+
+/-- Finite-type can be checked on a standard covering of the target. -/
+lemma Algebra.FiniteType.of_span_eq_top_target (s : Set S) (hs : Ideal.span (s : Set S) = ⊤)
+    (h : ∀ x ∈ s, Algebra.FiniteType R (Localization.Away x)) :
+    Algebra.FiniteType R S := by
+  obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
+  replace h (i : s) : Algebra.FiniteType R (Localization.Away i.val) := h i (h₁ i.property)
+  classical
+  -- Suppose `s : Finset S` spans `S`, and each `Sᵣ` is finitely generated as an `R`-algebra.
+  -- Say `t r : Finset Sᵣ` generates `Sᵣ`. By assumption, we may find `lᵢ` such that
+  -- `∑ lᵢ * sᵢ = 1`. I claim that all `s` and `l` and the numerators of `t` and generates `S`.
+  replace h := fun r => (h r).1
+  choose t ht using h
+  obtain ⟨l, hl⟩ :=
+    (Finsupp.mem_span_iff_linearCombination S (s : Set S) 1).mp
+      (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
+  let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (x : S)) (t x)
+  use s.attach.biUnion sf ∪ s ∪ l.support.image l
+  rw [_root_.eq_top_iff]
+  -- We need to show that every `x` falls in the subalgebra generated by those elements.
+  -- Since all `s` and `l` are in the subalgebra, it suffices to check that `sᵢ ^ nᵢ • x` falls in
+  -- the algebra for each `sᵢ` and some `nᵢ`.
+  rintro x -
+  apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
+  · intro x hx
+    apply Algebra.subset_adjoin
+    rw [Finset.coe_union, Finset.coe_union]
+    exact Or.inl (Or.inr hx)
+  · intro i
+    by_cases h : l i = 0; · rw [h]; exact zero_mem _
+    apply Algebra.subset_adjoin
+    rw [Finset.coe_union, Finset.coe_image]
+    exact Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))
+  · intro r
+    rw [Finset.coe_union, Finset.coe_union, Finset.coe_biUnion]
+    -- Since all `sᵢ` and numerators of `t r` are in the algebra, it suffices to show that the
+    -- image of `x` in `Sᵣ` falls in the `R`-adjoin of `t r`, which is of course true.
+    -- Porting note: The following `obtain` fails because Lean wants to know right away what the
+    -- placeholders are, so we need to provide a little more guidance
+    -- obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalization.exists_smul_mem_of_mem_adjoin
+    --   (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) _ _ _
+    rw [show ∀ A : Set S, (∃ n, (r : S) ^ n • x ∈ Algebra.adjoin R A) ↔
+      (∃ m : (Submonoid.powers (r : S)), (m : S) • x ∈ Algebra.adjoin R A) by
+      { exact fun _ => by simp [Submonoid.mem_powers_iff] }]
+    refine IsLocalization.exists_smul_mem_of_mem_adjoin
+      (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_
+    · intro x hx
+      apply Algebra.subset_adjoin
+      exact Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)
+    · rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
+      apply Algebra.subset_adjoin
+      exact Or.inl (Or.inr r.2)
+    · rw [ht]; trivial
+
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+lemma Algebra.FiniteType.of_span_eq_top_source (s : Set R) (hs : Ideal.span (s : Set R) = ⊤)
+    (h : ∀ i ∈ s, Algebra.FiniteType (Localization.Away i) (Localization.Away i ⊗[R] S)) :
+    Algebra.FiniteType R S := by
+  obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
+  replace h (i : s) := h i.val (h₁ i.property)
+  classical
+  letI := fun r : s => (Localization.awayMap (algebraMap R S) r).toAlgebra
+  set f := algebraMap R S
+  constructor
+  replace H := fun r => (h r).1
+  choose s₁ s₂ using H
+  let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)
+  use s.attach.biUnion sf
+  convert (Algebra.adjoin_attach_biUnion (R := R) sf).trans _
+  rw [eq_top_iff]
+  rintro x -
+  apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem
+    _ hs _ _
+  intro r
+  obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
+    multiple_mem_adjoin_of_mem_localization_adjoin (Submonoid.powers (r : R))
+      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away r.val ⊗[R] S))
+      (algebraMap S _ x) (by rw [s₂ r]; trivial)
+  rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
+  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
+    IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (Submonoid.powers (r : R)) _ (s₁ r) hn₁
+  rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
+  simp_rw [Submonoid.map_powers] at hn₂
+  use n₂ + n₁
+  exact le_iSup (fun x : s => Algebra.adjoin R (sf x : Set S)) r hn₂
+
+end Algebra