feat(RingTheory/StandardSmooth): pre-requisites for calculating the naive cotangent complex of a submersive presentation (#19749)

Preparations for #19748



Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

Author: chrisflav

Mathlib.lean

@@ -3366,6 +3366,7 @@ import Mathlib.LinearAlgebra.Basis.Basic
 import Mathlib.LinearAlgebra.Basis.Bilinear
 import Mathlib.LinearAlgebra.Basis.Cardinality
 import Mathlib.LinearAlgebra.Basis.Defs
+import Mathlib.LinearAlgebra.Basis.Exact
 import Mathlib.LinearAlgebra.Basis.Flag
 import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.LinearAlgebra.BilinearForm.Basic

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -543,6 +543,12 @@ theorem prod_disj_sum (s : Finset α) (t : Finset γ) (f : α ⊕ γ → β) :
   rw [← map_inl_disjUnion_map_inr, prod_disjUnion, prod_map, prod_map]
   rfl
 
+@[to_additive]
+lemma prod_sum_eq_prod_toLeft_mul_prod_toRight (s : Finset (α ⊕ γ)) (f : α ⊕ γ → β) :
+    ∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x) := by
+  rw [← Finset.toLeft_disjSum_toRight (u := s), Finset.prod_disj_sum, Finset.toLeft_disjSum,
+    Finset.toRight_disjSum]
+
 @[to_additive]
 theorem prod_sum_elim (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) :
     ∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x := by simp

Mathlib/Data/Matrix/Mul.lean

@@ -890,6 +890,24 @@ theorem vecMul_mulVec [Fintype m] [Fintype n] (A : Matrix m n α) (B : Matrix m
 
 end NonUnitalCommSemiring
 
+section Semiring
+
+variable [Semiring R]
+
+lemma mulVec_injective_of_isUnit [Fintype m] [DecidableEq m] {A : Matrix m m R}
+    (ha : IsUnit A) : Function.Injective A.mulVec := by
+  obtain ⟨B, hBl, hBr⟩ := isUnit_iff_exists.mp ha
+  intro x y hxy
+  simpa [hBr] using congrArg B.mulVec hxy
+
+lemma vecMul_injective_of_isUnit [Fintype m] [DecidableEq m] {A : Matrix m m R}
+    (ha : IsUnit A) : Function.Injective A.vecMul := by
+  obtain ⟨B, hBl, hBr⟩ := isUnit_iff_exists.mp ha
+  intro x y hxy
+  simpa [hBl] using congrArg B.vecMul hxy
+
+end Semiring
+
 section CommSemiring
 
 variable [CommSemiring α]

Mathlib/LinearAlgebra/Basis/Exact.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2024 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.Algebra.Exact
+import Mathlib.Algebra.Module.Submodule.Pointwise
+import Mathlib.LinearAlgebra.Basis.Basic
+
+/-!
+# Basis from a split exact sequence
+
+Let `0 → K → M → P → 0` be a split exact sequence of `R`-modules, let `s : M → K` be a
+retraction of `f` and `v` be a basis of `M` indexed by `κ ⊕ σ`. Then
+if `s vᵢ = 0` for `i : κ` and `(s vⱼ)ⱼ` is linear independent for `j : σ`, then
+the images of `vᵢ` for `i : κ` form a basis of `P`.
+
+We treat linear independence and the span condition separately. For convenience this
+is stated not for `κ ⊕ σ`, but for an arbitrary type `ι` with two maps `κ → ι` and `σ → ι`.
+-/
+
+variable {R M K P : Type*} [Ring R] [AddCommGroup M] [AddCommGroup K] [AddCommGroup P]
+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 : σ → ι}
+include hs hfg
+
+lemma LinearIndependent.linearIndependent_of_exact_of_retraction
+    (hainj : Function.Injective a) (hsa : ∀ i, s (v (a i)) = 0)
+    (hli : LinearIndependent R v) :
+    LinearIndependent R (g ∘ v ∘ a) := by
+  apply (LinearIndependent.comp hli a hainj).map
+  rw [Submodule.disjoint_def, hfg.linearMap_ker_eq]
+  rintro - hy ⟨y, rfl⟩
+  have hz : s (f y) = 0 := by
+    revert hy
+    generalize f y = x
+    intro hy
+    induction' hy using Submodule.span_induction with m hm
+    · obtain ⟨i, rfl⟩ := hm
+      apply hsa
+    all_goals simp_all
+  replace hs := DFunLike.congr_fun hs y
+  simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq] at hs
+  rw [← hs, hz, map_zero]
+
+private lemma top_le_span_of_aux (v : κ ⊕ σ → M)
+    (hg : Function.Surjective g) (hslzero : ∀ i, s (v (.inl i)) = 0)
+    (hli : LinearIndependent R (s ∘ v ∘ .inr)) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) :
+    ⊤ ≤ Submodule.span R (Set.range <| g ∘ v ∘ .inl) := by
+  rintro p -
+  obtain ⟨m, rfl⟩ := hg p
+  wlog h : m ∈ LinearMap.ker s
+  · let x : M := f (s m)
+    rw [show g m = g (m - f (s m)) by simp [hfg.apply_apply_eq_zero]]
+    apply this hs hfg v hg hslzero hli hsp
+    replace hs := DFunLike.congr_fun hs (s m)
+    simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq] at hs
+    simp [hs]
+  have : m ∈ Submodule.span R (Set.range v) := hsp trivial
+  obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp this
+  simp only [LinearMap.mem_ker, Finsupp.sum, map_sum, map_smul,
+    Finset.sum_sum_eq_sum_toLeft_add_sum_toRight, map_add, hslzero, smul_zero,
+    Finset.sum_const_zero, zero_add] at h
+  replace hli := (linearIndependent_iff'.mp hli) c.support.toRight (c ∘ .inr) h
+  simp only [Finset.mem_toRight, Finsupp.mem_support_iff, Function.comp_apply, not_imp_self] at hli
+  simp only [Finsupp.sum, Finset.sum_sum_eq_sum_toLeft_add_sum_toRight, hli, zero_smul,
+    Finset.sum_const_zero, add_zero, map_sum, map_smul]
+  exact Submodule.sum_mem _ (fun i hi ↦ Submodule.smul_mem _ _ <| Submodule.subset_span ⟨i, rfl⟩)
+
+lemma Submodule.top_le_span_of_exact_of_retraction (hg : Function.Surjective g)
+    (hsa : ∀ i, s (v (a i)) = 0) (hlib : LinearIndependent R (s ∘ v ∘ b))
+    (hab : Codisjoint (Set.range a) (Set.range b))
+    (hsp : ⊤ ≤ Submodule.span R (Set.range v)) :
+    ⊤ ≤ Submodule.span R (Set.range <| g ∘ v ∘ a) := by
+  apply top_le_span_of_aux hs hfg (Sum.elim (v ∘ a) (v ∘ b)) hg hsa hlib
+  simp only [codisjoint_iff, Set.sup_eq_union, Set.top_eq_univ] at hab
+  rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]
+
+/-- Let `0 → K → M → P → 0` be a split exact sequence of `R`-modules, let `s : M → K` be a
+retraction of `f` and `v` be a basis of `M` indexed by `κ ⊕ σ`. Then
+if `s vᵢ = 0` for `i : κ` and `(s vⱼ)ⱼ` is linear independent for `j : σ`, then
+the images of `vᵢ` for `i : κ` form a basis of `P`.
+
+For convenience this is stated for an arbitrary type `ι` with two maps `κ → ι` and `σ → ι`. -/
+noncomputable def Basis.ofSplitExact (hg : Function.Surjective g) (v : Basis ι R M)
+    (hainj : Function.Injective a) (hsa : ∀ i, s (v (a i)) = 0)
+    (hlib : LinearIndependent R (s ∘ v ∘ b))
+    (hab : Codisjoint (Set.range a) (Set.range b)) :
+    Basis κ R P :=
+  Basis.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]))

Mathlib/LinearAlgebra/Dimension/Free.lean

@@ -165,6 +165,11 @@ variable {M M'}
 
 namespace Module
 
+/-- A free module of rank zero is trivial. -/
+lemma subsingleton_of_rank_zero (h : Module.rank R M = 0) : Subsingleton M := by
+  rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h
+  exact (Module.Free.repr R M).subsingleton
+
 /-- See `rank_lt_aleph0` for the inverse direction without `Module.Free R M`. -/
 lemma rank_lt_aleph0_iff : Module.rank R M < ℵ₀ ↔ Module.Finite R M := by
   rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]

Mathlib/LinearAlgebra/Finsupp/Defs.lean

@@ -158,6 +158,7 @@ sending `l : β →₀ M` to the finitely supported function from `α` to `M` gi
 `l` with `f`.
 
 This is the linear version of `Finsupp.comapDomain`. -/
+@[simps]
 def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) →ₗ[R] α →₀ M where
   toFun l := Finsupp.comapDomain f l hf.injOn
   map_add' x y := by ext; simp

Mathlib/LinearAlgebra/Matrix/ToLin.lean

@@ -115,6 +115,11 @@ theorem Matrix.vecMul_injective_iff {R : Type*} [CommRing R] {M : Matrix m n R}
     ext j
     simp [vecMul, dotProduct]
 
+lemma Matrix.linearIndependent_rows_of_isUnit {R : Type*} [CommRing R] {A : Matrix m m R}
+    [DecidableEq m] (ha : IsUnit A) : LinearIndependent R (fun i ↦ A i) := by
+  rw [← Matrix.vecMul_injective_iff]
+  exact Matrix.vecMul_injective_of_isUnit ha
+
 section
 variable [DecidableEq m]
 
@@ -276,6 +281,12 @@ theorem Matrix.mulVec_injective_iff {R : Type*} [CommRing R] {M : Matrix m n R}
   change Function.Injective (fun x ↦ _) ↔ _
   simp_rw [← M.vecMul_transpose, vecMul_injective_iff]
 
+lemma Matrix.linearIndependent_cols_of_isUnit {R : Type*} [CommRing R] [Fintype m]
+    {A : Matrix m m R} [DecidableEq m] (ha : IsUnit A) :
+    LinearIndependent R (fun i ↦ A.transpose i) := by
+  rw [← Matrix.mulVec_injective_iff]
+  exact Matrix.mulVec_injective_of_isUnit ha
+
 end mulVec
 
 section ToMatrix'

Mathlib/RingTheory/Extension.lean

@@ -360,6 +360,10 @@ lemma Cotangent.val_mk (x : P.ker) : (mk x).val = Ideal.toCotangent _ x := rfl
 lemma Cotangent.mk_surjective : Function.Surjective (mk (P := P)) :=
   fun x ↦ Ideal.toCotangent_surjective P.ker x.val
 
+lemma Cotangent.mk_eq_zero_iff {P : Extension R S} (x : P.ker) :
+    Cotangent.mk x = 0 ↔ x.val ∈ P.ker ^ 2 := by
+  simp [Cotangent.ext_iff, Ideal.toCotangent_eq_zero]
+
 variable {P'}
 variable [Algebra R R'] [Algebra R' R''] [Algebra R' S'']
 variable [Algebra S S'] [Algebra S' S''] [Algebra S S'']

Mathlib/RingTheory/Presentation.lean

@@ -73,6 +73,11 @@ lemma aeval_val_relation (i) : aeval P.val (P.relation i) = 0 := by
   rw [← RingHom.mem_ker, ← P.ker_eq_ker_aeval_val, ← P.span_range_relation_eq_ker]
   exact Ideal.subset_span ⟨i, rfl⟩
 
+lemma relation_mem_ker (i : P.rels) : P.relation i ∈ P.ker := by
+  rw [← P.span_range_relation_eq_ker]
+  apply Ideal.subset_span
+  use i
+
 /-- The polynomial algebra wrt a family of generators modulo a family of relations. -/
 protected abbrev Quotient : Type (max w u) := P.Ring ⧸ P.ker
 

Mathlib/RingTheory/Smooth/StandardSmooth.lean

@@ -135,6 +135,17 @@ noncomputable def differential : (P.rels → P.Ring) →ₗ[P.Ring] (P.rels →
   Basis.constr P.basis P.Ring
     (fun j i : P.rels ↦ MvPolynomial.pderiv (P.map i) (P.relation j))
 
+/-- `PreSubmersivePresentation.differential` pushed forward to `S` via `aeval P.val`. -/
+noncomputable def aevalDifferential : (P.rels → S) →ₗ[S] (P.rels → S) :=
+  (Pi.basisFun S P.rels).constr S
+    (fun j i : P.rels ↦ aeval P.val <| pderiv (P.map i) (P.relation j))
+
+@[simp]
+lemma aevalDifferential_single [DecidableEq P.rels] (i j : P.rels) :
+    P.aevalDifferential (Pi.single i 1) j = aeval P.val (pderiv (P.map j) (P.relation i)) := by
+  dsimp only [aevalDifferential]
+  rw [← Pi.basisFun_apply, Basis.constr_basis]
+
 /-- The jacobian of a `P : PreSubmersivePresentation` is the determinant
 of `P.differential` viewed as element of `S`. -/
 noncomputable def jacobian : S :=
@@ -158,6 +169,13 @@ lemma jacobiMatrix_apply (i j : P.rels) :
     P.jacobiMatrix i j = MvPolynomial.pderiv (P.map i) (P.relation j) := by
   simp [jacobiMatrix, LinearMap.toMatrix, differential, basis]
 
+lemma aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix :
+    P.aevalDifferential.toMatrix' = (aeval P.val).mapMatrix P.jacobiMatrix := by
+  ext i j : 1
+  rw [← LinearMap.toMatrix_eq_toMatrix']
+  rw [LinearMap.toMatrix_apply]
+  simp [jacobiMatrix_apply]
+
 end Matrix
 
 section Constructions
@@ -262,11 +280,12 @@ the lower-right block has determinant jacobian of `P`.
 
 -/
 
-variable [Fintype (Q.comp P).rels]
+variable [DecidableEq (Q.comp P).rels] [Fintype (Q.comp P).rels]
 
 open scoped Classical in
 private lemma jacobiMatrix_comp_inl_inr (i : Q.rels) (j : P.rels) :
     (Q.comp P).jacobiMatrix (Sum.inl i) (Sum.inr j) = 0 := by
+  classical
   rw [jacobiMatrix_apply]
   refine MvPolynomial.pderiv_eq_zero_of_not_mem_vars (fun hmem ↦ ?_)
   apply MvPolynomial.vars_rename at hmem
@@ -279,7 +298,7 @@ private lemma jacobiMatrix_comp_₁₂ : (Q.comp P).jacobiMatrix.toBlocks₁₂
 
 section Q
 
-variable [Fintype Q.rels]
+variable [DecidableEq Q.rels] [Fintype Q.rels]
 
 open scoped Classical in
 private lemma jacobiMatrix_comp_inl_inl (i j : Q.rels) :
@@ -303,7 +322,7 @@ end Q
 
 section P
 
-variable [Fintype P.rels]
+variable [Fintype P.rels] [DecidableEq P.rels]
 
 open scoped Classical in
 private lemma jacobiMatrix_comp_inr_inr (i j : P.rels) :
@@ -471,6 +490,44 @@ end BaseChange
 
 end Constructions
 
+variable {R S}
+
+open Classical in
+/-- If `P` is submersive, `PreSubmersivePresentation.aevalDifferential` is an isomorphism. -/
+noncomputable def aevalDifferentialEquiv (P : SubmersivePresentation R S) :
+    (P.rels → S) ≃ₗ[S] (P.rels → S) :=
+  haveI : Fintype P.rels := Fintype.ofFinite P.rels
+  have : IsUnit (LinearMap.toMatrix (Pi.basisFun S P.rels) (Pi.basisFun S P.rels)
+        P.aevalDifferential).det := by
+    convert P.jacobian_isUnit
+    rw [LinearMap.toMatrix_eq_toMatrix', jacobian_eq_jacobiMatrix_det,
+      aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, P.algebraMap_eq]
+    simp [RingHom.map_det]
+  LinearEquiv.ofIsUnitDet this
+
+variable (P : SubmersivePresentation R S)
+
+@[simp]
+lemma aevalDifferentialEquiv_apply (x : P.rels → S) :
+    P.aevalDifferentialEquiv x = P.aevalDifferential x :=
+  rfl
+
+/-- If `P` is a submersive presentation, the partial derivatives of `P.relation i` by
+`P.map j` form a basis of `P.rels → S`. -/
+noncomputable def basisDeriv (P : SubmersivePresentation R S) : Basis P.rels S (P.rels → S) :=
+  Basis.map (Pi.basisFun S P.rels) P.aevalDifferentialEquiv
+
+@[simp]
+lemma basisDeriv_apply (i j : P.rels) :
+    P.basisDeriv i j = (aeval P.val) (pderiv (P.map j) (P.relation i)) := by
+  classical
+  simp [basisDeriv]
+
+lemma linearIndependent_aeval_val_pderiv_relation :
+    LinearIndependent S (fun i j ↦ (aeval P.val) (pderiv (P.map j) (P.relation i))) := by
+  simp_rw [← SubmersivePresentation.basisDeriv_apply]
+  exact P.basisDeriv.linearIndependent
+
 end SubmersivePresentation
 
 /--