painful progress…

DividedPowers/DPAlgebra/Dpow.lean

@@ -396,6 +396,10 @@ def Ψ : MvPolynomial S₀ A ⊗[A] DividedPowerAlgebra A (I →₀ A) →ₐ[A]
     ((Subalgebra.val S₀).comp (IsScalarTower.toAlgHom A (MvPolynomial S₀ A) S₀))
     (Φ A S hI)
 
+theorem Ψ_eq (i) (hi : i ∈ I) :
+    Ψ A S hI S₀ (Algebra.TensorProduct.includeRight (ι A _ (Finsupp.single ⟨i, hi⟩ 1 : I →₀ A))) = i := by
+  simp [Ψ, Φ, f, Basis.constr_apply]
+
 theorem Ψ_surjective : Function.Surjective (Ψ A S hI S₀) := by
   rw [← Algebra.range_top_iff_surjective _, eq_top_iff]
   intro s _
@@ -461,21 +465,22 @@ theorem _root_.DividedPowerAlgebra.T_free_and_D_to_QSplit :
   intro S _ _ I hI S₀ hIS₀
   let M := I →₀ A
   let R := MvPolynomial S₀ A
+  let D := DividedPowerAlgebra A M
   obtain ⟨hM, hM_eq⟩ := condD M
-  haveI hdpM_free : Module.Free A (DividedPowerAlgebra A M) := by
-    apply DividedPowerAlgebra.toModule_free
+  haveI hdpM_free : Module.Free A D := DividedPowerAlgebra.toModule_free A M
   haveI hR_free : Module.Free A R :=
     Module.Free.of_basis (MvPolynomial.basisMonomials _ _)
   -- We consider `R ⊗[A] DividedPowerAlgebra A M` as a comm ring and an A-algebra
-  let T := R ⊗[A] DividedPowerAlgebra A M
+  let T := R ⊗[A] D
   use T, by infer_instance, by infer_instance
   /- We need to add the fact that `R ⊗ DividedPowerAlgebra A M``
      is pregraduated in the sense of Roby
      The ideal is `K A ⊥ (augIdeal A M)`,
      that is, `R ⊗[A] augIdeal A M``
      hence it is a direct factor of R ⊗[A] DividedPowerAlgebra A M
-     (At this point, I wonder why one cannot prove
-      that the divided power algebra of a free module
+     (At this point, I wonder why one cannot use a different route,
+      proving base change first,
+      using that the divided power algebra of a free module
       has divided powers --- the relations come from combinatorics.)
       and then return DividedPowerAlgebra R (I →₀ R).)
      R mapsto S₀
@@ -492,61 +497,55 @@ theorem _root_.DividedPowerAlgebra.T_free_and_D_to_QSplit :
   use hK
   have : MvPolynomial S₀ A →ₐ[A] MvPolynomial S₀ A ⊗[A] DividedPowerAlgebra A M := by
     apply Algebra.TensorProduct.includeLeft
-  use (⊥ : Subalgebra (MvPolynomial S₀ A) T).restrictScalars A
-
+  -- the grade 0 part of our algebra `T`
+  use (⊥ : Subalgebra R T).restrictScalars A
+  -- it is a complement of the ideal `idK`
   refine ⟨?_, ?_⟩
   · rw [hidK]
-    have := Ideal.isAugmentation_baseChange (isCompl_augIdeal A M) (R := MvPolynomial S₀ A)
-    unfold Ideal.IsAugmentation at this ⊢
-    /- Unfortunately, `this` does not seem to be how we can get the desired property… -/
-    have isaugΓ : IsCompl
-      (Subalgebra.toSubmodule (⊥ : Subalgebra A _))
-      ((augIdeal A M).restrictScalars A) :=
-      isCompl_augIdeal A M
-
-    sorry
-  /- have : IsCompl
-    (Subalgebra.toSubmodule (Subalgebra.restrictScalars A ⊥)) (Submodule.restrictScalars A idK) := by
-    simp only [hidK]
-    have := Algebra.TensorProduct.lTensor_isCompl A R (S := DividedPowerAlgebra A M) (I := augIdeal A M) isaugΓ
-    sorry
-
+    obtain ⟨hd, hc⟩ := Ideal.isAugmentation_baseChange (isCompl_augIdeal A M) (R := MvPolynomial S₀ A)
+    apply IsCompl.mk
+    · simp only [Submodule.disjoint_def, Subalgebra.mem_toSubmodule, Submodule.restrictScalars_mem] at hd ⊢
+      intro x hx hx'
+      refine hd x ?_ hx'
+      rw [Algebra.mem_bot] at hx
+      obtain ⟨⟨x, hx⟩, rfl⟩ := hx
+      simp only [Subalgebra.mem_restrictScalars, Algebra.mem_bot] at hx
+      obtain ⟨x, rfl⟩ := hx
+      rw [Algebra.mem_bot]
+      exact ⟨x, rfl⟩
+    · simp only [codisjoint_iff, eq_top_iff]
+      intro x _
+      rw [Submodule.mem_sup]
+      obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.exists_add_eq_of_codisjoint hc x
+      refine ⟨y, ?_, z, hz, rfl⟩
+      rw [Subalgebra.mem_toSubmodule, Algebra.mem_bot] at hy ⊢
+      obtain ⟨y, rfl⟩ := hy
+      simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.id.map_eq_id,
+        RingHom.id_apply, Set.mem_range, Subtype.exists,
+        Subalgebra.mem_restrictScalars]
+      refine ⟨y ⊗ₜ[A] 1, ?_, rfl⟩
+      rw [Algebra.mem_bot, Set.mem_range]
+      exact ⟨y, rfl⟩
 
-  have : Subalgebra A (MvPolynomial S₀ A ⊗[A] DividedPowerAlgebra A M) :=
-    Subalgebra.map Algebra.TensorProduct.includeLeft ⊤
-  -- ???
-  have hisCompl : IsCompl
-      (Subalgebra.toSubmodule (Subalgebra.map Algebra.TensorProduct.includeLeft ⊤ : Subalgebra A (MvPolynomial S₀ A ⊗[A] DividedPowerAlgebra A M)))
-      (Submodule.restrictScalars A (K A ⊥ (augIdeal A M))) := by
-    simp only [Algebra.map_top, K, Ideal.map_bot, i2, ge_iff_le, bot_le, sup_of_le_right]
 
-    sorry
-  use sorry
-  use Subalgebra.map Algebra.TensorProduct.includeLeft ⊤
-  refine ?_
--/
-  -- the 0 part of our algebra
-
-
-  use sorry -- it is a complement
   use Ψ A S hI S₀
+  have hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I := by
+    convert (dpΨ A S hI S₀ condTFree hM hM_eq).ideal_comp
   constructor
-  · sorry
-    /- refine le_antisymm ?_ (dpΨ A S hI S₀ condTFree hM hM_eq).ideal_comp
+  · refine le_antisymm hI_le ?_
     intro i hi
     let m : M := Finsupp.single ⟨i, hi⟩ 1
-    have : i = Ψ A S hI (Algebra.TensorProduct.includeRight (ι A M m)) :=  by
-      simp [m, Ψ, Φ, f, Basis.constr_apply]
-    rw [this]
+    rw [← Ψ_eq A S hI S₀ i hi]
     apply Ideal.mem_map_of_mem
     apply Ideal.mem_sup_right
     apply Ideal.mem_map_of_mem
     apply ι_mem_augIdeal
-    sorry -/
+
   constructor
   · sorry -- Ψ maps the 0 part to S₀
   constructor
-  · apply Ψ_surjective A S hI S₀ hIS₀
+  · apply Ψ_surjective A S hI S₀
+    sorry
   constructor
   · exact (dpΨ A S hI S₀ condTFree hM hM_eq).isDPMorphism
   infer_instance -- tensor product of free modules is free

DividedPowers/DPAlgebra/Graded/GradeZero.lean

@@ -170,27 +170,6 @@ lemma augIdeal_isAugmentationIdeal' :
 
 
 
-/- We prove that the augmentation is an augmentation ideal,
-  namely there is a section
-  But we know what the section is!
-  BETTER : prove the precise `IsCompl` statement.  -/
-theorem augIdeal_isAugmentationIdeal :
-  IsAugmentation (augIdeal R M) := by
-  dsimp only [IsAugmentation]
-  use algebraMap_comp_kerLiftAlg R M
-  exact augIdeal_isAugmentationIdeal' R M
-
--- We prove that the augmentation is an augmentation ideal
--- as an algebra, namely there is a section which is an AlgHom
-theorem augIdeal_isAugmentationₐ :
-  IsAugmentationₐ R (augIdeal R M) := by
-  dsimp only [IsAugmentationₐ]
-  use {
-      toRingHom := algebraMap_comp_kerLiftAlg R M
-      commutes' := fun r ↦ by
-        simp [algebraMap_comp_kerLiftAlg] }
-  exact augIdeal_isAugmentationIdeal' R M
-
 -- Q : if algebra map has a section, is the kernel an augmentation ideal?
 theorem coeff_zero_of_mem_augIdeal {f : MvPolynomial (ℕ × M) R}
     (hf : f ∈ supported R {nm : ℕ × M | 0 < nm.fst}) (hf0 : mk f ∈ augIdeal R M) :
@@ -339,9 +318,7 @@ theorem grade0Subalgebra_eq_bot : grade0Subalgebra R M = ⊥ := by
   exact (algebraMap_right_inv_of_degree_zero R M ⟨p, hp⟩).symm
 
 theorem isCompl_augIdeal :
-    IsCompl
-      (Subalgebra.toSubmodule (⊥ : Subalgebra R _))
-      ((augIdeal R M).restrictScalars R) := by
+    Ideal.IsAugmentation R (augIdeal R M) := by
   apply IsCompl.mk
   · rw [Submodule.disjoint_def]
     intro x

DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean

@@ -18,9 +18,12 @@ then the ideal `R ⊗[A] I` of `R ⊗[A] S` is an augmentation ideal.
 
 * There is a weaker version that holds for general commutative rings
 and would just assert that the quotient map `R →+* R ⧸ I` has a section
-which is a ring homomorphism.
+which is a ring homomorphism (possibly with the variant “with data” that
+keeps track of the choice of one such section).
 
+## TODO
 
+Golf, dispatch
 
  -/
 
@@ -62,80 +65,66 @@ theorem Subalgebra.toSubmodule_restrictScalars_eq
   rfl
 
 end restrictScalars
-namespace Ideal
 
 open AlgHom RingHom Submodule Ideal.Quotient
 
-open TensorProduct
+open TensorProduct LinearMap
 
-/-- An ideal `J` of a commutative `R`-algebra `A` is an augmentation ideal
-  if this ideal is a complement to `⊥ : Subalgebra R A` -/
-def IsAugmentation (R : Type*) [CommRing R]
-    {A : Type*} [CommRing A] [Algebra R A] (J : Ideal A) : Prop :=
-  IsCompl (Subalgebra.toSubmodule (⊥ : Subalgebra R A)) (J.restrictScalars R)
-
-theorem _root_.LinearMap.ker_lTensor_of_linearProjOfIsCompl
+theorem LinearMap.ker_lTensor_of_linearProjOfIsCompl
     {M : Type*} [AddCommGroup M] [Module A M]
     {M₁ M₂ : Submodule A M} (hM : IsCompl M₁ M₂)
     (Q : Type*) [AddCommGroup Q] [Module A Q] :
-    LinearMap.ker (LinearMap.lTensor Q (Submodule.linearProjOfIsCompl _ _ hM))
-    = LinearMap.range (LinearMap.lTensor Q M₂.subtype) := by
-  rw [← LinearMap.exact_iff]
+    ker (lTensor Q (linearProjOfIsCompl _ _ hM)) = range (lTensor Q M₂.subtype) := by
+  rw [← exact_iff]
   apply lTensor_exact
-  simp only [LinearMap.exact_iff, Submodule.range_subtype, linearProjOfIsCompl_ker]
-  simp only [← LinearMap.range_eq_top, Submodule.linearProjOfIsCompl_range]
+  simp only [exact_iff, range_subtype, linearProjOfIsCompl_ker]
+  simp only [← range_eq_top, linearProjOfIsCompl_range]
 
-theorem _root_.LinearMap.ker_baseChange_of_linearProjOfIsCompl
+theorem LinearMap.ker_baseChange_of_linearProjOfIsCompl
     {M : Type*} [AddCommGroup M] [Module A M]
     {M₁ M₂ : Submodule A M} (hM : IsCompl M₁ M₂)
     (R : Type*) [CommRing R] [Algebra A R] :
-    LinearMap.ker (LinearMap.baseChange R (Submodule.linearProjOfIsCompl _ _ hM))
-    = LinearMap.range (LinearMap.baseChange R M₂.subtype) := by
-  simpa only [←LinearMap.exact_iff] using LinearMap.ker_lTensor_of_linearProjOfIsCompl hM R
+    ker (baseChange R (linearProjOfIsCompl _ _ hM)) = range (baseChange R M₂.subtype) := by
+  simpa only [← exact_iff] using ker_lTensor_of_linearProjOfIsCompl hM R
 
-theorem _root_.LinearMap.isCompl_lTensor
+theorem LinearMap.isCompl_lTensor
     {M : Type*} [AddCommGroup M] [Module A M]
     {M₁ M₂ : Submodule A M} (hM : IsCompl M₁ M₂)
     (Q : Type*) [AddCommGroup Q] [Module A Q] :
-    IsCompl
-      (LinearMap.range (LinearMap.lTensor Q M₁.subtype))
-      (LinearMap.range (LinearMap.lTensor Q M₂.subtype)) := by
+    IsCompl (range (lTensor Q M₁.subtype)) (range (lTensor Q M₂.subtype)) := by
   have hq :
-    M₁.subtype.comp (Submodule.linearProjOfIsCompl _ _ hM)
-      + M₂.subtype.comp (Submodule.linearProjOfIsCompl _ _ hM.symm) = LinearMap.id := by
+    M₁.subtype.comp (linearProjOfIsCompl _ _ hM)
+      + M₂.subtype.comp (linearProjOfIsCompl _ _ hM.symm) = id := by
     ext x
-    simp only [LinearMap.add_apply, LinearMap.coe_comp, coeSubtype, Function.comp_apply,
-      LinearMap.id_coe, id_eq]
-    rw [Submodule.linear_proj_add_linearProjOfIsCompl_eq_self]
+    simp only [add_apply, coe_comp, coeSubtype, Function.comp_apply,
+      id_coe, id_eq]
+    rw [linear_proj_add_linearProjOfIsCompl_eq_self]
   apply IsCompl.mk
-  · rw [Submodule.disjoint_def]
+  · rw [disjoint_def]
     intro x h h'
-    rw [← LinearMap.id_apply x (R := A), ← LinearMap.lTensor_id, ← hq]
-    simp only [LinearMap.lTensor_add, LinearMap.lTensor_comp,
+    rw [← id_apply x (R := A), ← lTensor_id, ← hq]
+    simp only [lTensor_add, lTensor_comp,
       LinearMap.add_apply, LinearMap.coe_comp, Function.comp_apply]
-    rw [← LinearMap.ker_lTensor_of_linearProjOfIsCompl hM Q] at h'
-    rw [← LinearMap.ker_lTensor_of_linearProjOfIsCompl hM.symm Q] at h
-    rw [LinearMap.mem_ker] at h h'
+    rw [← ker_lTensor_of_linearProjOfIsCompl hM Q] at h'
+    rw [← ker_lTensor_of_linearProjOfIsCompl hM.symm Q] at h
+    rw [mem_ker] at h h'
     simp only [h', _root_.map_zero, h, add_zero]
   · rw [codisjoint_iff]
     rw [eq_top_iff]
     intro x _
-    rw [← LinearMap.lTensor_id_apply Q _ x, ← hq]
-    simp only [LinearMap.lTensor_add, LinearMap.lTensor_comp,
-      LinearMap.add_apply, LinearMap.coe_comp, Function.comp_apply]
+    rw [← lTensor_id_apply Q _ x, ← hq]
+    simp only [lTensor_add, lTensor_comp, add_apply, coe_comp, Function.comp_apply]
     exact Submodule.add_mem _
-      (Submodule.mem_sup_left (LinearMap.mem_range_self _ _))
-      (Submodule.mem_sup_right (LinearMap.mem_range_self _ _))
+      (mem_sup_left (LinearMap.mem_range_self _ _))
+      (mem_sup_right (LinearMap.mem_range_self _ _))
 
-theorem _root_.LinearMap.isCompl_baseChange
+theorem LinearMap.isCompl_baseChange
     {M : Type*} [AddCommGroup M] [Module A M]
     {M₁ M₂ : Submodule A M} (hM : IsCompl M₁ M₂)
     (R : Type*) [CommRing R] [Algebra A R] :
-    IsCompl
-      (LinearMap.range (LinearMap.baseChange R M₁.subtype))
-      (LinearMap.range (LinearMap.baseChange R M₂.subtype)) := by
-  rw [← Submodule.isCompl_restrictScalars_iff A]
-  exact _root_.LinearMap.isCompl_lTensor hM R
+    IsCompl (range (baseChange R M₁.subtype)) (range (baseChange R M₂.subtype)) := by
+  rw [← isCompl_restrictScalars_iff A]
+  exact isCompl_lTensor hM R
 
 theorem Algebra.baseChange_bot {R S : Type*} [CommRing R] [Algebra A R] [CommRing S] [Algebra A S] :
     Subalgebra.toSubmodule ⊥ =
@@ -150,33 +139,34 @@ theorem Algebra.baseChange_bot {R S : Type*} [CommRing R] [Algebra A R] [CommRin
     induction y using TensorProduct.induction_on with
     | zero =>
       use 0
-      simp only [TensorProduct.zero_tmul, LinearMap.map_zero]
+      simp only [zero_tmul, LinearMap.map_zero]
       simp
     | tmul r s =>
       rcases s with ⟨s, hs⟩
       simp only [Subalgebra.mem_toSubmodule] at hs
       obtain ⟨a, rfl⟩ := hs
       use a • r
       simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.id.map_eq_id, RingHom.id_apply,
-        toRingHom_eq_coe, coe_coe, LinearMap.baseChange_tmul, coeSubtype]
-      simp only [TensorProduct.smul_tmul]
+        toRingHom_eq_coe, coe_coe, baseChange_tmul, coeSubtype]
+      simp only [smul_tmul]
       rw [Algebra.ofId_apply, Algebra.algebraMap_eq_smul_one]
     | add x y hx hy =>
       obtain ⟨x', hx⟩ := hx
       obtain ⟨y', hy⟩ := hy
       use x' + y'
-      simp only [TensorProduct.add_tmul, hx, hy, map_add]
+      simp only [add_tmul, hx, hy, map_add]
 
 theorem Algebra.TensorProduct.map_includeRight_eq_range_baseChange
-    {R S : Type*} [CommRing R] [Algebra A R] [CommRing S] [Algebra A S]
-    {I : Ideal S} :
-    Submodule.restrictScalars R (map Algebra.TensorProduct.includeRight I)
+    {S : Type*} [CommRing S] [Algebra A S] {I : Ideal S}
+    (R : Type*) [CommRing R] [Algebra A R]  :
+    Submodule.restrictScalars R (I.map Algebra.TensorProduct.includeRight)
     = LinearMap.range (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) := by
   ext x
-  simp only [Submodule.restrictScalars_mem, LinearMap.mem_range]
+  simp only [restrictScalars_mem, LinearMap.mem_range]
   constructor
   · intro hx
-    apply Submodule.span_induction hx (p := fun x ↦ ∃ y, (LinearMap.baseChange R (Submodule.subtype (Submodule.restrictScalars A I))) y = x )
+    apply Submodule.span_induction hx
+      (p := fun x ↦ ∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x )
     · rintro x ⟨s, hs, rfl⟩; use 1 ⊗ₜ[A] ⟨s, hs⟩; rfl
     · use 0; simp only [_root_.map_zero]
     · rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩; use x + y; simp only [map_add]
@@ -187,11 +177,10 @@ theorem Algebra.TensorProduct.map_includeRight_eq_range_baseChange
         induction a using TensorProduct.induction_on with
         | zero =>
           use 0
-          simp only [_root_.map_zero, LinearMap.baseChange_tmul,
-            Submodule.coeSubtype, smul_eq_mul, zero_mul]
+          simp only [_root_.map_zero, baseChange_tmul, coeSubtype, smul_eq_mul, zero_mul]
         | tmul u v =>
           use (u * r) ⊗ₜ[A] (v • s)
-          simp only [LinearMap.baseChange_tmul, Submodule.coeSubtype, smul_eq_mul,
+          simp only [baseChange_tmul, coeSubtype, smul_eq_mul,
             Algebra.TensorProduct.tmul_mul_tmul]
           rw [Submodule.coe_smul, smul_eq_mul]
         | add u v hu hv =>
@@ -210,7 +199,7 @@ theorem Algebra.TensorProduct.map_includeRight_eq_range_baseChange
     | tmul r s =>
       rcases s with ⟨s, hs⟩
       simp only [restrictScalars_mem] at hs
-      simp only [LinearMap.baseChange_tmul, coeSubtype]
+      simp only [baseChange_tmul, coeSubtype]
       rw [← mul_one r, ← smul_eq_mul, ← TensorProduct.smul_tmul']
       rw [← IsScalarTower.algebraMap_smul (R ⊗[A] S) r, smul_eq_mul]
       apply Ideal.mul_mem_left
@@ -219,8 +208,14 @@ theorem Algebra.TensorProduct.map_includeRight_eq_range_baseChange
       simp only [map_add]
       exact Ideal.add_mem _ hx hy
 
+/-- An ideal `J` of a commutative `R`-algebra `A` is an augmentation ideal
+  if this ideal is a complement to `⊥ : Subalgebra R A` -/
+def Ideal.IsAugmentation (R : Type*) [CommRing R]
+    {A : Type*} [CommRing A] [Algebra R A] (J : Ideal A) : Prop :=
+  IsCompl (Subalgebra.toSubmodule (⊥ : Subalgebra R A)) (J.restrictScalars R)
+
 /-- The base change of an algebra with an augmentation ideal -/
-theorem _root_.Ideal.isAugmentation_baseChange
+theorem Ideal.isAugmentation_baseChange
     {S : Type*} [CommRing S] [Algebra A S]
     {I : Ideal S}
     (hI : IsCompl (Subalgebra.toSubmodule (⊥ : Subalgebra A S)) (I.restrictScalars A))
@@ -230,7 +225,7 @@ theorem _root_.Ideal.isAugmentation_baseChange
   unfold Ideal.IsAugmentation
   rw [Algebra.baseChange_bot]
   rw [Algebra.TensorProduct.map_includeRight_eq_range_baseChange]
-  exact LinearMap.isCompl_baseChange hI R
+  exact isCompl_baseChange hI R
 
 #exit
 -- OLD VERSION