feat(ring_theory/ring_hom/finite): Finite type is a local property (#15379)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

src/algebra/algebra/subalgebra/basic.lean

@@ -5,6 +5,8 @@ Authors: Kenny Lau, Yury Kudryashov
 -/
 import algebra.algebra.basic
 import data.set.Union_lift
+import linear_algebra.finsupp
+import ring_theory.ideal.operations
 
 /-!
 # Subalgebras over Commutative Semiring
@@ -1064,6 +1066,39 @@ set_like.ext' (set.centralizer_univ A)
 
 end centralizer
 
+/-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` in `S`, and `S'` a subalgebra of `S` that contains
+`lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
+`r ^ n • x ∈ M'` for some `n` for each `r : s`. -/
+lemma mem_of_span_eq_top_of_smul_pow_mem {S : Type*} [comm_ring S] [algebra R S]
+  (S' : subalgebra R S) (s : set S) (l : s →₀ S) (hs : finsupp.total s S S coe l = 1)
+  (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S)
+  (H : ∀ r : s, ∃ (n : ℕ), (r ^ n : S) • x ∈ S') : x ∈ S' :=
+begin
+  let s' : set S' := coe ⁻¹' s,
+  let e : s' ≃ s := ⟨λ x, ⟨x.1, x.2⟩, λ x, ⟨⟨_, hs' x.2⟩, x.2⟩, λ ⟨⟨_, _⟩, _⟩, rfl, λ ⟨_, _⟩, rfl⟩,
+  let l' : s →₀ S' := ⟨l.support, λ x, ⟨_, hl x⟩,
+    λ _, finsupp.mem_support_iff.trans $ iff.not $ by { rw ← subtype.coe_inj, refl }⟩,
+  have : ideal.span s' = ⊤,
+  { rw [ideal.eq_top_iff_one, ideal.span, finsupp.mem_span_iff_total],
+    refine ⟨finsupp.equiv_map_domain e.symm l', subtype.ext $ eq.trans _ hs⟩,
+    rw finsupp.total_equiv_map_domain,
+    exact finsupp.apply_total _ (algebra.of_id S' S).to_linear_map _ _ },
+  obtain ⟨s'', hs₁, hs₂⟩ := (ideal.span_eq_top_iff_finite _).mp this,
+  replace H : ∀ r : s'', ∃ (n : ℕ), (r ^ n : S) • x ∈ S' := λ r, H ⟨r, hs₁ r.2⟩,
+  choose n₁ n₂ using H,
+  let N := s''.attach.sup n₁,
+  have hs' := ideal.span_pow_eq_top _ hs₂ N,
+  have : ∀ {x : S}, x ∈ (algebra.of_id S' S).range.to_submodule ↔ x ∈ S' :=
+    λ x, ⟨by { rintro ⟨x, rfl⟩, exact x.2 }, λ h, ⟨⟨x, h⟩, rfl⟩⟩,
+  rw ← this,
+  apply (algebra.of_id S' S).range.to_submodule.mem_of_span_top_of_smul_mem _ hs',
+  rintro ⟨_, r, hr, rfl⟩,
+  convert submodule.smul_mem _ (r ^ (N - n₁ ⟨r, hr⟩)) (this.mpr $ n₂ ⟨r, hr⟩) using 1,
+  simp only [_root_.coe_coe, subtype.coe_mk,
+    subalgebra.smul_def, smul_smul, ← pow_add, subalgebra.coe_pow],
+  rw tsub_add_cancel_of_le (finset.le_sup (s''.mem_attach _) : n₁ ⟨r, hr⟩ ≤ N),
+end
+
 end subalgebra
 
 section nat

src/ring_theory/adjoin/basic.lean

@@ -270,8 +270,13 @@ begin
   congr' 1 with z, simp [submonoid.closure_union, submonoid.mem_sup, set.mem_mul]
 end
 
-lemma 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) :=
+variable {R}
+
+lemma pow_smul_mem_of_smul_subset_of_mem_adjoin
+  [comm_semiring B] [algebra R B] [algebra A B] [is_scalar_tower R A B]
+  (r : A) (s : set B) (B' : subalgebra R B) (hs : r • s ⊆ B') {x : B} (hx : x ∈ adjoin R s)
+  (hr : algebra_map A B r ∈ B') :
+  ∃ n₀ : ℕ, ∀ n ≥ n₀, r ^ n • x ∈ B' :=
 begin
   change x ∈ (adjoin R s).to_submodule at hx,
   rw [adjoin_eq_span, finsupp.mem_span_iff_total] at hx,
@@ -280,16 +285,24 @@ begin
   use l.support.sup n₁,
   intros n hn,
   rw finsupp.smul_sum,
-  refine (adjoin R (r • s)).to_submodule.sum_mem _,
+  refine B'.to_submodule.sum_mem _,
   intros 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, smul_smul _ (l a), mul_comm,
-    ← smul_smul, adjoin_eq_span],
-  refine submodule.smul_mem _ _ _,
-  exact submodule.smul_mem _ _ (submodule.subset_span (n₂ a))
+  rw [← tsub_add_cancel_of_le this, pow_add, ← smul_smul,
+    ← is_scalar_tower.algebra_map_smul A (l a) (a : B), smul_smul (r ^ n₁ a),
+    mul_comm, ← smul_smul, smul_def, map_pow, is_scalar_tower.algebra_map_smul],
+  apply subalgebra.mul_mem _ (subalgebra.pow_mem _ hr _) _,
+  refine subalgebra.smul_mem _ _ _,
+  change _ ∈ B'.to_submonoid,
+  rw ← submonoid.closure_eq B'.to_submonoid,
+  apply submonoid.closure_mono hs (n₂ a),
 end
 
+lemma 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.algebra_map_mem _ _)
+
 end comm_semiring
 
 section ring

src/ring_theory/local_properties.lean

@@ -111,9 +111,24 @@ def ring_hom.holds_for_localization_away : Prop :=
 ∀ ⦃R : Type u⦄ (S : Type u) [comm_ring R] [comm_ring S] [by exactI algebra R S] (r : R)
   [by exactI is_localization.away r S], by exactI P (algebra_map R S)
 
-/-- A property `P` of ring homs satisfies `ring_hom.of_localization_span_target`
+/-- A property `P` of ring homs satisfies `ring_hom.of_localization_finite_span_target`
 if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `S` such that
-`P` holds for `R →+* Sᵣ`. -/
+`P` holds for `R →+* Sᵣ`.
+
+Note that this is equivalent to `ring_hom.of_localization_span_target` via
+`ring_hom.of_localization_span_target_iff_finite`, but this is easier to prove. -/
+def ring_hom.of_localization_finite_span_target : Prop :=
+∀ ⦃R S : Type u⦄ [comm_ring R] [comm_ring S] (f : by exactI R →+* S)
+  (s : finset S) (hs : by exactI ideal.span (s : set S) = ⊤)
+  (H : by exactI (∀ (r : s), P ((algebra_map S (localization.away (r : S))).comp f))),
+  by exactI P f
+
+/-- A property `P` of ring homs satisfies `ring_hom.of_localization_span_target`
+if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `S` such that
+`P` holds for `R →+* Sᵣ`.
+
+Note that this is equivalent to `ring_hom.of_localization_finite_span_target` via
+`ring_hom.of_localization_span_target_iff_finite`, but this has less restrictions when applying. -/
 def ring_hom.of_localization_span_target : Prop :=
 ∀ ⦃R S : Type u⦄ [comm_ring R] [comm_ring S] (f : by exactI R →+* S)
   (s : set S) (hs : by exactI ideal.span s = ⊤)
@@ -148,6 +163,19 @@ begin
     exact h s' h₂ (λ x, hs' ⟨_, h₁ x.prop⟩) }
 end
 
+lemma ring_hom.of_localization_span_target_iff_finite :
+  ring_hom.of_localization_span_target @P ↔ ring_hom.of_localization_finite_span_target @P :=
+begin
+  delta ring_hom.of_localization_span_target ring_hom.of_localization_finite_span_target,
+  apply forall₅_congr, -- TODO: Using `refine` here breaks `resetI`.
+  introsI,
+  split,
+  { intros h s, exact h s },
+  { intros h s hs hs',
+    obtain ⟨s', h₁, h₂⟩ := (ideal.span_eq_top_iff_finite s).mp hs,
+    exact h s' h₂ (λ x, hs' ⟨_, h₁ x.prop⟩) }
+end
+
 variables {P f R' S'}
 
 lemma _root_.ring_hom.property_is_local.respects_iso (hP : ring_hom.property_is_local @P) :
@@ -543,6 +571,37 @@ lemma localization_away_map_finite_type (r : R) [is_localization.away r R']
     (is_localization.away.map R' S' f r).finite_type :=
 localization_finite_type.away r hf
 
+variable {S'}
+
+/--
+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`.
+-/
+lemma is_localization.exists_smul_mem_of_mem_adjoin [algebra R S]
+  [algebra R S'] [is_scalar_tower R S S'] (M : submonoid S)
+  [is_localization M S'] (x : S) (s : finset S') (A : subalgebra R S)
+  (hA₁ : (is_localization.finset_integer_multiple M s : set S) ⊆ A)
+  (hA₂ : M ≤ A.to_submonoid)
+  (hx : algebra_map S S' x ∈ algebra.adjoin R (s : set S')) :
+    ∃ m : M, m • x ∈ A :=
+begin
+  let g : S →ₐ[R] S' := is_scalar_tower.to_alg_hom R S S',
+  let y := is_localization.common_denom_of_finset M s,
+  have hx₁ : (y : S) • ↑s = g '' _ := (is_localization.finset_integer_multiple_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_subset _ hA₁ }) hx (set.mem_image_of_mem _ (hA₂ y.2)),
+  obtain ⟨x', hx', hx''⟩ := hn n (le_of_eq rfl),
+  rw [algebra.smul_def, ← _root_.map_mul] at hx'',
+  obtain ⟨a, ha₂⟩ := (is_localization.eq_iff_exists M S').mp hx'',
+  use a * y ^ n,
+  convert A.mul_mem hx' (hA₂ a.2),
+  convert ha₂.symm,
+  simp only [submonoid.smul_def, submonoid.coe_pow, smul_eq_mul, submonoid.coe_mul],
+  ring,
+end
+
 /--
 Let `S` be an `R`-algebra, `M` an 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`,
@@ -556,30 +615,10 @@ lemma is_localization.lift_mem_adjoin_finset_integer_multiple [algebra R S]
     ∃ m : M, m • x ∈ algebra.adjoin R
       (is_localization.finset_integer_multiple (M.map (algebra_map R S : R →* S)) s : set S) :=
 begin
-  -- mirrors the proof of `is_localization.smul_mem_finset_integer_multiple_span`
-  let g : S →ₐ[R] S' := alg_hom.mk' (algebra_map S S')
-    (λ c x, by simp [algebra.algebra_map_eq_smul_one]),
-
-  let y := is_localization.common_denom_of_finset (M.map (algebra_map R S : R →* S)) s,
-  have hx₁ : (y : S) • ↑s = g '' _ := (is_localization.finset_integer_multiple_image _ s).symm,
-  obtain ⟨y', hy', e : algebra_map R S y' = y⟩ := y.prop,
-  have : algebra_map R S y' • (s : set S') = y' • s :=
-    by simp_rw [algebra.algebra_map_eq_smul_one, smul_assoc, one_smul],
-  rw [← e, this] at hx₁,
-  replace hx₁ := congr_arg (algebra.adjoin R) hx₁,
-  obtain ⟨n, hn⟩ := algebra.pow_smul_mem_adjoin_smul _ y' (s : set S') hx,
-  specialize hn n (le_of_eq rfl),
-  erw [hx₁, ← g.map_smul, ← g.map_adjoin] at hn,
-  obtain ⟨x', hx', hx''⟩ := hn,
-  obtain ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ := (is_localization.eq_iff_exists
-    (M.map (algebra_map R S : R →* S)) S').mp hx'',
-  use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M) ^ n,
-  convert (algebra.adjoin R (is_localization.finset_integer_multiple
-    (submonoid.map (algebra_map R S : R →* S) M) s : set S)).smul_mem hx' a using 1,
-  convert ha₂.symm,
-  { rw [mul_comm (y' ^ n • x), subtype.coe_mk, submonoid.smul_def, submonoid.coe_mul, ← smul_smul,
-      algebra.smul_def, submonoid_class.coe_pow], refl },
-  { rw mul_comm, exact algebra.smul_def _ _ }
+  obtain ⟨⟨_, a, ha, rfl⟩, e⟩ := is_localization.exists_smul_mem_of_mem_adjoin
+    (M.map (algebra_map R S : R →* S)) x s (algebra.adjoin R _) algebra.subset_adjoin _ hx,
+  { exact ⟨⟨a, ha⟩, by simpa [submonoid.smul_def] using e⟩ },
+{ rintros _ ⟨a, ha, rfl⟩, exact subalgebra.algebra_map_mem _ a }
 end
 
 lemma finite_type_of_localization_span : ring_hom.of_localization_span @ring_hom.finite_type :=
@@ -613,7 +652,7 @@ begin
   rw [submonoid.smul_def, algebra.smul_def, is_scalar_tower.algebra_map_apply R S,
     subtype.coe_mk, ← map_mul] at hn₁,
   obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := is_localization.lift_mem_adjoin_finset_integer_multiple
-    (submonoid.powers (r : R)) (localization.away (f r)) _ (s₁ r) hn₁,
+    (submonoid.powers (r : R)) _ (s₁ r) hn₁,
   rw [submonoid.smul_def, ← algebra.smul_def, smul_smul, subtype.coe_mk, ← pow_add] at hn₂,
   use n₂ + n₁,
   refine le_supr (λ (x : s), algebra.adjoin R (sf x : set S)) r _,

src/ring_theory/ring_hom/finite_type.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2021 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import ring_theory.local_properties
+import ring_theory.localization.inv_submonoid
+
+/-!
+
+# The meta properties of finite-type ring homomorphisms.
+
+The main result is `ring_hom.finite_is_local`.
+
+-/
+
+namespace ring_hom
+
+open_locale pointwise
+
+lemma finite_type_stable_under_composition :
+  stable_under_composition @finite_type :=
+by { introv R hf hg, exactI hg.comp hf }
+
+lemma finite_type_holds_for_localization_away :
+  holds_for_localization_away @finite_type :=
+begin
+  introv R _,
+  resetI,
+  suffices : algebra.finite_type R S,
+  { change algebra.finite_type _ _, convert this, ext, rw algebra.smul_def, refl },
+  exact is_localization.finite_type_of_monoid_fg (submonoid.powers r) S,
+end
+
+lemma finite_type_of_localization_span_target : of_localization_span_target @finite_type :=
+begin
+  -- Setup algebra intances.
+  rw of_localization_span_target_iff_finite,
+  introv R hs H,
+  resetI,
+  classical,
+  letI := f.to_algebra,
+  replace H : ∀ r : s, algebra.finite_type R (localization.away (r : S)),
+  { intro r, convert H r, ext, rw algebra.smul_def, refl },
+  replace H := λ r, (H r).1,
+  constructor,
+  -- 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`.
+  choose t ht using H,
+  obtain ⟨l, hl⟩ := (finsupp.mem_span_iff_total S (s : set S) 1).mp
+    (show (1 : S) ∈ ideal.span (s : set S), by { rw hs, trivial }),
+  let sf := λ (x : s), is_localization.finset_integer_multiple (submonoid.powers (x : S)) (t x),
+  use s.attach.bUnion sf ∪ s ∪ l.support.image l,
+  rw 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 _,
+  { intros x hx,
+    apply algebra.subset_adjoin,
+    rw [finset.coe_union, finset.coe_union],
+    exact or.inl (or.inr hx) },
+  { intros 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_bUnion],
+    -- 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.
+    obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := is_localization.exists_smul_mem_of_mem_adjoin
+      (submonoid.powers (r : S)) x (t r)
+      (algebra.adjoin R _) _ _ _,
+    { exact ⟨n₂, hn₂⟩ },
+    { intros x hx,
+      apply algebra.subset_adjoin,
+      refine 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 } }
+end
+
+lemma finite_is_local :
+  property_is_local @finite_type :=
+⟨localization_finite_type, finite_type_of_localization_span_target,
+  finite_type_stable_under_composition, finite_type_holds_for_localization_away⟩
+
+end ring_hom