feat(ring_theory/ring_hom/surjective): Meta properties about the surjectivity of ring homomorphisms (#17292)

Also generalize several lemmas

Author: erdOne

src/algebra/algebra/subalgebra/basic.lean

@@ -1057,36 +1057,41 @@ 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' :=
+lemma mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type*} [comm_ring S]
+  [algebra R S] (S' : subalgebra R S) {ι : Type*} (ι' : finset ι) (s : ι → S) (l : ι → S)
+  (e : ∑ i in ι', l i * s i = 1)
+  (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
+  (H : ∀ i, ∃ (n : ℕ), (s i ^ 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' = ⊤,
+  classical,
+  suffices : x ∈ (algebra.of_id S' S).range.to_submodule,
+  { obtain ⟨x, rfl⟩ := this, exact x.2 },
+  choose n hn using H,
+  let s' : ι → S' := λ x, ⟨s x, hs x⟩,
+  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,
+    refine ⟨(finsupp.of_support_finite (λ i : ι', (⟨l i, hl i⟩ : S')) (set.to_finite _))
+      .map_domain $ λ i, ⟨s' i, i, i.2, rfl⟩, S'.to_submodule.injective_subtype _⟩,
+    rw [finsupp.total_map_domain, finsupp.total_apply, finsupp.sum_fintype,
+      map_sum, submodule.subtype_apply, subalgebra.coe_one],
+    { exact finset.sum_attach.trans e },
+    { exact λ _, zero_smul _ _ } },
+  let N := ι'.sup n,
+  have hs' := ideal.span_pow_eq_top _ this N,
   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),
+  rintros ⟨_, _, ⟨i, hi, rfl⟩, rfl⟩,
+  change s i ^ N • x ∈ _,
+  rw [← tsub_add_cancel_of_le (show n i ≤ N, from finset.le_sup hi), pow_add, mul_smul],
+  refine submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') _,
+  exact ⟨⟨_, hn i⟩, rfl⟩,
 end
 
+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' :=
+mem_of_finset_sum_eq_one_of_pow_smul_mem S' l.support coe l hs (λ x, hs' x.2) hl x H
+
 end subalgebra
 
 section nat

src/algebra/module/projective.lean

@@ -121,8 +121,7 @@ begin
   use coprod (lmap_domain R R (inl R P Q)) (lmap_domain R R (inr R P Q)) ∘ₗ sP.prod_map sQ,
   ext; simp only [coe_inl, coe_inr, coe_comp, function.comp_app, prod_map_apply, map_zero,
     coprod_apply, lmap_domain_apply, map_domain_zero, add_zero, zero_add, id_comp,
-    total_map_domain R _ (prod.mk.inj_right (0 : Q)),
-    total_map_domain R _ (prod.mk.inj_left (0 : P))],
+    total_map_domain],
 
   { rw [←fst_apply _, apply_total R], exact hsP x, },
   { rw [←snd_apply _, apply_total R], exact finsupp.total_zero_apply _ (sP x), },
@@ -148,7 +147,7 @@ begin
   use dfinsupp.coprod_map f ∘ₗ dfinsupp.map_range.linear_map s,
 
   ext i x j,
-  simp only [dfinsupp.coprod_map, direct_sum.lof, total_map_domain R _ dfinsupp.single_injective,
+  simp only [dfinsupp.coprod_map, direct_sum.lof, total_map_domain,
     coe_comp, coe_lsum, id_coe, linear_equiv.coe_to_linear_map, finsupp_lequiv_dfinsupp_symm_apply,
     function.comp_app, dfinsupp.lsingle_apply, dfinsupp.map_range.linear_map_apply,
     dfinsupp.map_range_single, lmap_domain_apply, dfinsupp.to_finsupp_single,

src/linear_algebra/finsupp.lean

@@ -493,23 +493,21 @@ theorem lmap_domain_total (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v
   (finsupp.total α' M' R v').comp (lmap_domain R R f) = g.comp (finsupp.total α M R v) :=
 by ext l; simp [total_apply, finsupp.sum_map_domain_index, add_smul, h]
 
+theorem total_comp_lmap_domain (f : α → α') :
+  (finsupp.total α' M' R v').comp (finsupp.lmap_domain R R f) = (finsupp.total α M' R (v' ∘ f)) :=
+by { ext, simp }
+
 @[simp] theorem total_emb_domain (f : α ↪ α') (l : α →₀ R) :
   (finsupp.total α' M' R v') (emb_domain f l) = (finsupp.total α M' R (v' ∘ f)) l :=
 by simp [total_apply, finsupp.sum, support_emb_domain, emb_domain_apply]
 
-theorem total_map_domain (f : α → α') (hf : function.injective f) (l : α →₀ R) :
+@[simp] theorem total_map_domain (f : α → α') (l : α →₀ R) :
   (finsupp.total α' M' R v') (map_domain f l) = (finsupp.total α M' R (v' ∘ f)) l :=
-begin
-  have : map_domain f l = emb_domain ⟨f, hf⟩ l,
-  { rw emb_domain_eq_map_domain ⟨f, hf⟩,
-    refl },
-  rw this,
-  apply total_emb_domain R ⟨f, hf⟩ l
-end
+linear_map.congr_fun (total_comp_lmap_domain _ _) l
 
 @[simp] theorem total_equiv_map_domain (f : α ≃ α') (l : α →₀ R) :
   (finsupp.total α' M' R v') (equiv_map_domain f l) = (finsupp.total α M' R (v' ∘ f)) l :=
-by rw [equiv_map_domain_eq_map_domain, total_map_domain _ _ f.injective]
+by rw [equiv_map_domain_eq_map_domain, total_map_domain]
 
 /-- A version of `finsupp.range_total` which is useful for going in the other direction -/
 theorem span_eq_range_total (s : set M) :

src/linear_algebra/linear_independent.lean

@@ -882,8 +882,7 @@ begin
   { dsimp only [l],
     rw finsupp.total_map_domain,
     rw (hv.comp f f.injective).total_repr,
-    { refl },
-    { exact f.injective } },
+    { refl } },
   have h_total_eq : (finsupp.total ι M R v) l = (finsupp.total ι M R v) (finsupp.single i 1),
     by rw [h_total_l, finsupp.total_single, one_smul],
   have l_eq : l = _ := linear_map.ker_eq_bot.1 hv h_total_eq,

src/ring_theory/ring_hom/surjective.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2022 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
+
+/-!
+
+# The meta properties of surjective ring homomorphisms.
+
+-/
+
+namespace ring_hom
+
+open_locale tensor_product
+
+open tensor_product algebra.tensor_product
+
+local notation `surjective` := λ {X Y : Type*} [comm_ring X] [comm_ring Y] ,
+  by exactI λ (f : X →+* Y), function.surjective f
+
+lemma surjective_stable_under_composition :
+  stable_under_composition surjective :=
+by { introv R hf hg, exactI hg.comp hf }
+
+lemma surjective_respects_iso :
+  respects_iso surjective :=
+begin
+  apply surjective_stable_under_composition.respects_iso,
+  introsI,
+  exact e.surjective
+end
+
+lemma surjective_stable_under_base_change :
+  stable_under_base_change surjective :=
+begin
+  classical,
+  introv R h,
+  resetI,
+  intro x,
+  induction x using tensor_product.induction_on with x y x y ex ey,
+  { exact ⟨0, map_zero _⟩ },
+  { obtain ⟨y, rfl⟩ := h y, use y • x, dsimp,
+    rw [tensor_product.smul_tmul, algebra.algebra_map_eq_smul_one] },
+  { obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ⟨ex, ey⟩, exact ⟨x + y, map_add _ x y⟩ }
+end
+
+open_locale big_operators
+
+lemma surjective_of_localization_span :
+  of_localization_span surjective :=
+begin
+  introv R hs H,
+  resetI,
+  letI := f.to_algebra,
+  show function.surjective (algebra.of_id R S),
+  rw [← algebra.range_top_iff_surjective, eq_top_iff],
+  rintro x -,
+  obtain ⟨l, hl⟩ :=
+    (finsupp.mem_span_iff_total R s 1).mp (show _ ∈ ideal.span s, by { rw hs, trivial }),
+  fapply subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem _
+    l.support (λ x : s, f x) (λ x : s, f (l x)),
+  { dsimp only, simp_rw [← _root_.map_mul, ← map_sum, ← f.map_one], exact f.congr_arg hl },
+  { exact λ _, set.mem_range_self _ },
+  { exact λ _, set.mem_range_self _ },
+  { intro r,
+    obtain ⟨y, hy⟩ := H r (is_localization.mk' _ x (1 : submonoid.powers (f r))),
+    obtain ⟨z, ⟨_, n, rfl⟩, rfl⟩ := is_localization.mk'_surjective (submonoid.powers (r : R)) y,
+    erw [is_localization.map_mk', is_localization.eq] at hy,
+    obtain ⟨⟨_, m, rfl⟩, hm⟩ := hy,
+    dsimp at hm,
+    simp_rw [_root_.mul_assoc, _root_.one_mul, ← map_pow, ← f.map_mul, ← pow_add, mul_comm x] at hm,
+    rw map_pow at hm,
+    refine ⟨n + m, _, hm⟩ }
+end
+
+end ring_hom