feat(RingTheory/Kaehler): Cotangent complex associated to an embedding into affine space. (#14859)

Co-authored-by: Andrew Yang <[email protected]>

Author: erdOne

Mathlib.lean

@@ -3790,6 +3790,7 @@ import Mathlib.RingTheory.IsTensorProduct
 import Mathlib.RingTheory.Jacobson
 import Mathlib.RingTheory.JacobsonIdeal
 import Mathlib.RingTheory.Kaehler.Basic
+import Mathlib.RingTheory.Kaehler.CotangentComplex
 import Mathlib.RingTheory.Kaehler.Polynomial
 import Mathlib.RingTheory.LaurentSeries
 import Mathlib.RingTheory.LittleWedderburn

Mathlib/Algebra/Exact.lean

@@ -355,6 +355,22 @@ theorem Exact.split_tfae
 
 end split
 
+section Prod
+
+variable [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N]
+
+lemma Exact.inr_fst : Function.Exact (LinearMap.inr R M N) (LinearMap.fst R M N) := by
+  rintro ⟨x, y⟩
+  simp only [LinearMap.fst_apply, @eq_comm _ x, LinearMap.coe_inr, Set.mem_range, Prod.mk.injEq,
+    exists_eq_right]
+
+lemma Exact.inl_snd : Function.Exact (LinearMap.inl R M N) (LinearMap.snd R M N) := by
+  rintro ⟨x, y⟩
+  simp only [LinearMap.snd_apply, @eq_comm _ y, LinearMap.coe_inl, Set.mem_range, Prod.mk.injEq,
+    exists_eq_left]
+
+end Prod
+
 section Ring
 
 open LinearMap Submodule

Mathlib/LinearAlgebra/Dual.lean

@@ -1697,7 +1697,7 @@ theorem dualDistrib_dualDistribInvOfBasis_left_inverse (b : Basis ι R M) (c : B
     Basis.tensorProduct_apply, coeFn_sum, Finset.sum_apply, smul_apply, LinearEquiv.coe_coe,
     map_tmul, lid_tmul, smul_eq_mul, id_coe, id_eq]
   rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
-  · simp
+  · simpa using mul_comm _ _
   all_goals { intros; simp [*] at * }
 
 -- Porting note: introduced to help with timeout in dualDistribEquivOfBasis

Mathlib/LinearAlgebra/TensorProduct/Basis.lean

@@ -18,6 +18,8 @@ noncomputable section
 
 open Set LinearMap Submodule
 
+open scoped TensorProduct
+
 section CommSemiring
 
 variable {R : Type*} {S : Type*} {M : Type*} {N : Type*} {ι : Type*} {κ : Type*}
@@ -26,26 +28,43 @@ variable {R : Type*} {S : Type*} {M : Type*} {N : Type*} {ι : Type*} {κ : Type
 
 /-- If `b : ι → M` and `c : κ → N` are bases then so is `fun i ↦ b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N`. -/
 def Basis.tensorProduct (b : Basis ι S M) (c : Basis κ R N) :
-    Basis (ι × κ) S (TensorProduct R M N) :=
+    Basis (ι × κ) S (M ⊗[R] N) :=
   Finsupp.basisSingleOne.map
     ((TensorProduct.AlgebraTensorModule.congr b.repr c.repr).trans <|
         (finsuppTensorFinsupp R S _ _ _ _).trans <|
           Finsupp.lcongr (Equiv.refl _) (TensorProduct.AlgebraTensorModule.rid R S S)).symm
 
 @[simp]
-theorem Basis.tensorProduct_apply (b : Basis ι R M) (c : Basis κ R N) (i : ι) (j : κ) :
+theorem Basis.tensorProduct_apply (b : Basis ι S M) (c : Basis κ R N) (i : ι) (j : κ) :
     Basis.tensorProduct b c (i, j) = b i ⊗ₜ c j := by
   simp [Basis.tensorProduct]
 
-theorem Basis.tensorProduct_apply' (b : Basis ι R M) (c : Basis κ R N) (i : ι × κ) :
+theorem Basis.tensorProduct_apply' (b : Basis ι S M) (c : Basis κ R N) (i : ι × κ) :
     Basis.tensorProduct b c i = b i.1 ⊗ₜ c i.2 := by
   simp [Basis.tensorProduct]
 
 @[simp]
-theorem Basis.tensorProduct_repr_tmul_apply (b : Basis ι R M) (c : Basis κ R N) (m : M) (n : N)
+theorem Basis.tensorProduct_repr_tmul_apply (b : Basis ι S M) (c : Basis κ R N) (m : M) (n : N)
     (i : ι) (j : κ) :
-    (Basis.tensorProduct b c).repr (m ⊗ₜ n) (i, j) = b.repr m i * c.repr n j := by
+    (Basis.tensorProduct b c).repr (m ⊗ₜ n) (i, j) = c.repr n j • b.repr m i := by
   simp [Basis.tensorProduct, mul_comm]
 
+variable (S)
+
+/-- The lift of an `R`-basis of `M` to an `S`-basis of the base change `S ⊗[R] M`. -/
+noncomputable
+def Basis.baseChange (b : Basis ι R M) : Basis ι S (S ⊗[R] M) :=
+  ((Basis.singleton Unit S).tensorProduct b).reindex (Equiv.punitProd ι)
+
+@[simp]
+lemma Basis.baseChange_repr_tmul (b : Basis ι R M) (x y i) :
+    (b.baseChange S).repr (x ⊗ₜ y) i = b.repr y i • x := by
+  simp [Basis.baseChange, Basis.tensorProduct]
+
+@[simp]
+lemma Basis.baseChange_apply (b : Basis ι R M) (i) :
+    b.baseChange S i = 1 ⊗ₜ b i := by
+  simp [Basis.baseChange, Basis.tensorProduct]
+
 end CommSemiring
 end

Mathlib/LinearAlgebra/TensorProduct/Matrix.lean

@@ -40,6 +40,7 @@ theorem TensorProduct.toMatrix_map (f : M →ₗ[R] M') (g : N →ₗ[R] N') :
   ext ⟨i, j⟩ ⟨i', j'⟩
   simp_rw [Matrix.kroneckerMap_apply, toMatrix_apply, Basis.tensorProduct_apply,
     TensorProduct.map_tmul, Basis.tensorProduct_repr_tmul_apply]
+  exact mul_comm _ _
 
 /-- The matrix built from `Matrix.kronecker` corresponds to the linear map built from
 `TensorProduct.map`. -/
@@ -54,20 +55,18 @@ theorem TensorProduct.toMatrix_comm :
     toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM) (TensorProduct.comm R M N) =
       (1 : Matrix (ι × κ) (ι × κ) R).submatrix Prod.swap _root_.id := by
   ext ⟨i, j⟩ ⟨i', j'⟩
-  simp_rw [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, TensorProduct.comm_tmul,
-    Basis.tensorProduct_repr_tmul_apply, Matrix.submatrix_apply, Basis.repr_self,
-    Finsupp.single_apply, @eq_comm _ j', @eq_comm _ i', mul_ite, mul_one, mul_zero,
-    Matrix.one_apply, Prod.swap_prod_mk, _root_.id, Prod.ext_iff, ite_and]
+  simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, comm_tmul,
+    Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ i',
+    @eq_comm _ j', smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, and_comm, submatrix_apply,
+    Matrix.one_apply, Prod.swap_prod_mk, id_eq, Prod.mk.injEq]
 
 /-- `TensorProduct.assoc` corresponds to a permutation of the identity matrix. -/
 theorem TensorProduct.toMatrix_assoc :
     toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP))
         (TensorProduct.assoc R M N P) =
       (1 : Matrix (ι × κ × τ) (ι × κ × τ) R).submatrix _root_.id (Equiv.prodAssoc _ _ _) := by
   ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩
-  simp_rw [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe,
-    TensorProduct.assoc_tmul, Basis.tensorProduct_repr_tmul_apply, Matrix.submatrix_apply,
-    Basis.repr_self, Finsupp.single_apply, @eq_comm _ i', @eq_comm _ j', @eq_comm _ k',
-    mul_ite, mul_one, mul_zero, Matrix.one_apply, _root_.id, Equiv.prodAssoc_apply, Prod.ext_iff,
-    ite_and]
-  split_ifs <;> simp
+  simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, assoc_tmul,
+    Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ k',
+    @eq_comm _ j', smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, @eq_comm _ i',
+    submatrix_apply, Matrix.one_apply, id_eq, Equiv.prodAssoc_apply, Prod.mk.injEq]

Mathlib/RingTheory/Generators.lean

@@ -222,7 +222,7 @@ variable [Algebra R R''] [Algebra S S''] [Algebra R S'']
   [IsScalarTower R R'' S''] [IsScalarTower R S S'']
 variable [Algebra R' R''] [Algebra S' S''] [Algebra R' S'']
   [IsScalarTower R' R'' S''] [IsScalarTower R' S' S'']
-variable [IsScalarTower R' R'' R''] [IsScalarTower S S' S'']
+variable [IsScalarTower R R' R''] [IsScalarTower S S' S'']
 
 section Hom
 
@@ -266,6 +266,10 @@ lemma Hom.toAlgHom_X (f : Hom P P') (i) : f.toAlgHom (.X i) = f.val i :=
 lemma Hom.toAlgHom_C (f : Hom P P') (r) : f.toAlgHom (.C r) = .C (algebraMap _ _ r) :=
   MvPolynomial.aeval_C f.val r
 
+lemma Hom.toAlgHom_monomial (f : Generators.Hom P P') (v r) :
+    f.toAlgHom (monomial v r) = r • v.prod (f.val · ^ ·) := by
+  rw [toAlgHom, aeval_monomial, Algebra.smul_def]
+
 /-- Giving a hom between two families of generators is equivalent to
 giving an algebra homomorphism between the polynomial rings. -/
 @[simps]
@@ -290,6 +294,9 @@ instance : Inhabited (Hom P P') := ⟨defaultHom P P'⟩
 @[simps]
 protected noncomputable def Hom.id : Hom P P := ⟨X, by simp⟩
 
+@[simp]
+lemma Hom.toAlgHom_id : Hom.toAlgHom (.id P) = AlgHom.id _ _ := by ext1; simp
+
 variable {P P' P''}
 
 /-- The composition of two homs. -/
@@ -310,6 +317,14 @@ lemma Hom.comp_id (f : Hom P P') : f.comp (Hom.id P) = f := by ext; simp
 @[simp]
 lemma Hom.id_comp (f : Hom P P') : (Hom.id P').comp f = f := by ext; simp [Hom.id, aeval_X_left]
 
+@[simp]
+lemma Hom.toAlgHom_comp_apply (f : Hom P P') (g : Hom P' P'') (x) :
+    (g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x) := by
+  induction x using MvPolynomial.induction_on with
+  | h_C r => simp only [← MvPolynomial.algebraMap_eq, AlgHom.map_algebraMap]
+  | h_add x y hx hy => simp only [map_add, hx, hy]
+  | h_X p i hp => simp only [_root_.map_mul, hp, toAlgHom_X, comp_val]; rfl
+
 variable {T} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
 
 /-- Given families of generators `X ⊆ T` over `S` and `Y ⊆ S` over `R`,
@@ -374,6 +389,7 @@ variable (x y : P.Cotangent) (w z : P.ker.Cotangent)
 @[simp] lemma of_zero : (of 0 : P.Cotangent) = 0 := rfl
 @[simp] lemma of_val : of x.val = x := rfl
 @[simp] lemma val_of : (of w).val = w := rfl
+@[simp] lemma val_sub : (x - y).val = x.val - y.val := rfl
 
 end Cotangent
 
@@ -466,6 +482,21 @@ lemma Cotangent.map_mk (f : Hom P P') (x) :
       .mk ⟨f.toAlgHom x, by simpa [-map_aeval] using RingHom.congr_arg (algebraMap S S') x.2⟩ :=
   rfl
 
+@[simp]
+lemma Cotangent.map_id :
+    Cotangent.map (.id P) = LinearMap.id := by
+  ext x
+  obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
+  simp only [map_mk, Hom.toAlgHom_id, AlgHom.coe_id, id_eq, Subtype.coe_eta, val_mk,
+    LinearMap.id_coe]
+
+lemma Cotangent.map_comp (f : Hom P P') (g : Hom P' P'') :
+    Cotangent.map (g.comp f) = (map g).restrictScalars S ∘ₗ map f := by
+  ext x
+  obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
+  simp only [map_mk, val_mk, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
+    Function.comp_apply, Hom.toAlgHom_comp_apply]
+
 end Cotangent
 
 end Algebra.Generators