feat(RingTheory/Extension/Cotangent): presentation is submersive if I/I² has a suitable basis (#28769)

Let `P` be a presentation of an algebra with kernel `I`. We show that if `I/I²` has a basis given by the images of the relations and the module of Kaehler differentials has a basis given by the differentials of the free generators (those that don't appear in the Jacobian matrix), then `P` is submersive.

We will later deduce from this a presentation-independent characterization of standard smooth algebras.

From Pi1.

Author: chrisflav

Mathlib.lean

@@ -5662,6 +5662,7 @@ import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Extension
 import Mathlib.RingTheory.Extension.Basic
 import Mathlib.RingTheory.Extension.Cotangent.Basic
+import Mathlib.RingTheory.Extension.Cotangent.Free
 import Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
 import Mathlib.RingTheory.Extension.Generators
 import Mathlib.RingTheory.Extension.Presentation.Basic

Mathlib/Algebra/Group/Subgroup/Map.lean

@@ -253,13 +253,23 @@ theorem map_inf_eq (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f)
 theorem map_bot (f : G →* N) : (⊥ : Subgroup G).map f = ⊥ :=
   (gc_map_comap f).l_bot
 
+@[to_additive]
+lemma disjoint_map {f : G →* N} (hf : Function.Injective f) {H K : Subgroup G} (h : Disjoint H K) :
+    Disjoint (H.map f) (K.map f) := by
+  rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
+
 @[to_additive]
 theorem map_top_of_surjective (f : G →* N) (h : Function.Surjective f) : Subgroup.map f ⊤ = ⊤ := by
   rw [eq_top_iff]
   intro x _
   obtain ⟨y, hy⟩ := h x
   exact ⟨y, trivial, hy⟩
 
+@[to_additive]
+lemma codisjoint_map {f : G →* N} (hf : Function.Surjective f)
+    {H K : Subgroup G} (h : Codisjoint H K) : Codisjoint (H.map f) (K.map f) := by
+  rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, map_top_of_surjective _ hf]
+
 @[to_additive (attr := simp)]
 lemma map_equiv_top {F : Type*} [EquivLike F G N] [MulEquivClass F G N] (f : F) :
     map (f : G →* N) ⊤ = ⊤ :=
@@ -560,6 +570,11 @@ end MonoidHom
 
 namespace Subgroup
 
+@[to_additive]
+lemma surjOn_iff_le_map {f : G →* N} {H : Subgroup G} {K : Subgroup N} :
+    Set.SurjOn f H K ↔ K ≤ H.map f :=
+  Iff.rfl
+
 @[to_additive (attr := simp)]
 theorem equivMapOfInjective_coe_mulEquiv (H : Subgroup G) (e : G ≃* G') :
     H.equivMapOfInjective (e : G →* G') (EquivLike.injective e) = e.subgroupMap H := by

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -312,6 +312,11 @@ theorem comap_iInf {ι : Sort*} (f : F) (s : ι → Submonoid N) :
 theorem map_bot (f : F) : (⊥ : Submonoid M).map f = ⊥ :=
   (gc_map_comap f).l_bot
 
+@[to_additive]
+lemma disjoint_map {f : F} (hf : Function.Injective f) {H K : Submonoid M} (h : Disjoint H K) :
+    Disjoint (H.map f) (K.map f) := by
+  rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
+
 @[to_additive (attr := simp)]
 theorem comap_top (f : F) : (⊤ : Submonoid N).comap f = ⊤ :=
   (gc_map_comap f).u_top
@@ -848,6 +853,11 @@ end MonoidHom
 
 namespace Submonoid
 
+@[to_additive]
+lemma surjOn_iff_le_map {f : M →* N} {H : Submonoid M} {K : Submonoid N} :
+    Set.SurjOn f H K ↔ K ≤ H.map f :=
+  Iff.rfl
+
 open MonoidHom
 
 @[to_additive]
@@ -946,6 +956,13 @@ theorem bot_or_nontrivial (S : Submonoid M) : S = ⊥ ∨ Nontrivial S := by
 theorem bot_or_exists_ne_one (S : Submonoid M) : S = ⊥ ∨ ∃ x ∈ S, x ≠ (1 : M) :=
   S.bot_or_nontrivial.imp_right S.nontrivial_iff_exists_ne_one.mp
 
+@[to_additive]
+lemma codisjoint_map {F : Type*} [FunLike F M N] [MonoidHomClass F M N] {f : F}
+    (hf : Function.Surjective f) {H K : Submonoid M} (h : Codisjoint H K) :
+    Codisjoint (H.map f) (K.map f) := by
+  rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map,
+    mrange_eq_top_of_surjective _ hf]
+
 section Pi
 
 variable {ι : Type*} {M : ι → Type*} [∀ i, MulOneClass (M i)]

Mathlib/Algebra/Module/Submodule/LinearMap.lean

@@ -144,6 +144,9 @@ theorem domRestrict_apply (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) (
     f.domRestrict p x = f x :=
   rfl
 
+lemma coe_domRestrict (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) :
+    ⇑(f.domRestrict p) = Set.restrict p f := rfl
+
 /-- A linear map `f : M₂ → M` whose values lie in a submodule `p ⊆ M` can be restricted to a
 linear map M₂ → p.
 

Mathlib/Algebra/Module/Submodule/Map.lean

@@ -232,6 +232,10 @@ theorem map_iSup {ι : Sort*} (f : F) (p : ι → Submodule R M) :
     map f (⨆ i, p i) = ⨆ i, map f (p i) :=
   (gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup
 
+lemma disjoint_map {f : F} (hf : Function.Injective f) {p q : Submodule R M} (hpq : Disjoint p q) :
+    Disjoint (p.map f) (q.map f) := by
+  rw [disjoint_iff, ← map_inf f hf, disjoint_iff.mp hpq, map_bot]
+
 end
 
 @[simp]
@@ -593,6 +597,10 @@ theorem inf_comap_le_comap_add (f₁ f₂ : M →ₛₗ[τ₁₂] M₂) :
   change f₁ m ∈ q ∧ f₂ m ∈ q at h
   apply q.add_mem h.1 h.2
 
+lemma surjOn_iff_le_map [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M}
+    {q : Submodule R₂ M₂} : Set.SurjOn f p q ↔ q ≤ p.map f :=
+  Iff.rfl
+
 end Submodule
 
 namespace Submodule

Mathlib/Algebra/Module/Submodule/Range.lean

@@ -363,6 +363,11 @@ def mapIic (p : Submodule R M) :
     (p.mapIic q : Submodule R M) = q.map p.subtype :=
   rfl
 
+lemma codisjoint_map [RingHomSurjective τ₁₂] {f : F} (hf : Function.Surjective f)
+    {p q : Submodule R M} (hpq : Codisjoint p q) : Codisjoint (p.map f) (q.map f) := by
+  rw [codisjoint_iff, ← Submodule.map_sup, codisjoint_iff.mp hpq, map_top,
+    LinearMap.range_eq_top_of_surjective f hf]
+
 end AddCommMonoid
 
 end Submodule

Mathlib/Analysis/InnerProductSpace/Symmetric.lean

@@ -271,7 +271,7 @@ theorem _root_.Submodule.IsCompl.projection_isSymmetric_iff
   refine ⟨fun h u hu v hv => ?_, fun h x y => ?_⟩
   · rw [← Subtype.coe_mk u hu, ← Subtype.coe_mk v hv,
       ← Submodule.linearProjOfIsCompl_apply_left hUV ⟨u, hu⟩, ← U.subtype_apply, ← comp_apply,
-      ← h, comp_apply, linearProjOfIsCompl_apply_right hUV ⟨v, hv⟩,
+      ← h, comp_apply, Submodule.linearProjOfIsCompl_apply_right hUV ⟨v, hv⟩,
       map_zero, inner_zero_left]
   · nth_rw 2 [← hUV.projection_add_projection_eq_self x]
     nth_rw 1 [← hUV.projection_add_projection_eq_self y]

Mathlib/Data/Finsupp/Basic.lean

@@ -707,6 +707,14 @@ theorem comapDomain_mapDomain (hf : Function.Injective f) (l : α →₀ M) :
     comapDomain f (mapDomain f l) hf.injOn = l := by
   ext; rw [comapDomain_apply, mapDomain_apply hf]
 
+lemma mem_range_mapDomain_iff (hf : Function.Injective f) (x : β →₀ M) :
+    x ∈ Set.range (Finsupp.mapDomain f) ↔ ∀ b ∉ Set.range f, x b = 0 := by
+  refine ⟨fun ⟨y, hy⟩ x hx ↦ hy ▸ Finsupp.mapDomain_notin_range y x hx, fun h ↦ ?_⟩
+  refine ⟨Finsupp.comapDomain f x hf.injOn, Finsupp.mapDomain_comapDomain f hf _ fun i hi ↦ ?_⟩
+  by_contra hc
+  simp only [Finset.mem_coe, Finsupp.mem_support_iff, ne_eq] at hi
+  exact hi (h _ hc)
+
 end FInjective
 
 end ComapDomain

Mathlib/LinearAlgebra/Basis/Exact.lean

@@ -5,6 +5,7 @@ Authors: Christian Merten
 -/
 import Mathlib.Algebra.Exact
 import Mathlib.LinearAlgebra.Basis.Basic
+import Mathlib.LinearAlgebra.Projection
 
 /-!
 # Basis from a split exact sequence
@@ -23,6 +24,8 @@ variable [Module R M] [Module R K] [Module R P]
 variable {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K}
 variable (hs : s ∘ₗ f = LinearMap.id) (hfg : Function.Exact f g)
 variable {ι κ σ : Type*} {v : ι → M} {a : κ → ι} {b : σ → ι}
+
+section
 include hs hfg
 
 lemma LinearIndependent.linearIndependent_of_exact_of_retraction
@@ -91,3 +94,39 @@ noncomputable def Module.Basis.ofSplitExact (hg : Function.Surjective g) (v : Ba
     Basis κ R P :=
   .mk (v.linearIndependent.linearIndependent_of_exact_of_retraction hs hfg hainj hsa)
     (Submodule.top_le_span_of_exact_of_retraction hs hfg hg hsa hlib hab (by rw [v.span_eq]))
+
+end
+
+section
+include hfg
+
+lemma Submodule.linearProjOfIsCompl_comp_surjective_of_exact
+    {p q : Submodule R M} (hpq : IsCompl p q)
+    (hmap : Submodule.map g q = ⊤) :
+    Function.Surjective (Submodule.linearProjOfIsCompl p q hpq ∘ₗ f) := by
+  rw [← Set.surjOn_univ, LinearMap.coe_comp, Set.surjOn_comp_iff, Set.image_univ]
+  rw [← LinearMap.coe_range, ← Submodule.top_coe (R := R), surjOn_iff_le_map,
+    ← hfg.linearMap_ker_eq]
+  intro x triv
+  obtain ⟨a, haq, ha⟩ : g x.val ∈ q.map g := by rwa [hmap]
+  exact ⟨x - a, by simp [← ha], by simpa⟩
+
+lemma Submodule.linearProjOfIsCompl_comp_bijective_of_exact
+    (hf : Function.Injective f) {p q : Submodule R M} (hpq : IsCompl p q)
+    (hker : Disjoint (LinearMap.ker g) q) (hmap : Submodule.map g q = ⊤) :
+    Function.Bijective (Submodule.linearProjOfIsCompl p q hpq ∘ₗ f) := by
+  refine ⟨?_, Submodule.linearProjOfIsCompl_comp_surjective_of_exact hfg _ hmap⟩
+  rwa [LinearMap.coe_comp, Set.InjOn.injective_iff ↑(LinearMap.range f) _ subset_rfl]
+  simpa [← LinearMap.disjoint_ker_iff_injOn, ← hfg.linearMap_ker_eq]
+
+lemma LinearMap.linearProjOfIsCompl_comp_bijective_of_exact
+    (hf : Function.Injective f) {q : Submodule R M} {E : Type*} [AddCommGroup E] [Module R E]
+    {i : E →ₗ[R] M} (hi : Function.Injective i) (h : IsCompl (LinearMap.range i) q)
+    (hker : Disjoint (LinearMap.ker g) q) (hmap : Submodule.map g q = ⊤) :
+    Function.Bijective (LinearMap.linearProjOfIsCompl q i hi h ∘ₗ f) := by
+  rw [LinearMap.linearProjOfIsCompl, LinearMap.comp_assoc, LinearMap.coe_comp,
+      Function.Bijective.of_comp_iff]
+  · exact (LinearEquiv.ofInjective i hi).symm.bijective
+  · exact Submodule.linearProjOfIsCompl_comp_bijective_of_exact hfg hf h hker hmap
+
+end

Mathlib/LinearAlgebra/Finsupp/Defs.lean

@@ -147,6 +147,9 @@ theorem lmapDomain_apply (f : α → α') (l : α →₀ M) :
     (lmapDomain M R f : (α →₀ M) →ₗ[R] α' →₀ M) l = mapDomain f l :=
   rfl
 
+lemma coe_lmapDomain (f : α → α') : ⇑(lmapDomain M R f) = Finsupp.mapDomain f :=
+  rfl
+
 @[simp]
 theorem lmapDomain_id : (lmapDomain M R _root_.id : (α →₀ M) →ₗ[R] α →₀ M) = LinearMap.id :=
   LinearMap.ext fun _ => mapDomain_id