progress on dpow_comp

DividedPowers/DPAlgebra/Dpow.lean

@@ -1124,8 +1124,9 @@ theorem dpow_ι (A : Type u) [CommRing A] [DecidableEq A] (M : Type u) [AddCommG
     (x : M) (n : ℕ) : dpow (dividedPowers' A M) n (ι A M x) = dp A n x :=
   (condD_holds A M).choose_spec n x
 
-example (A : Type u) [CommRing A] [DecidableEq A] (M : Type u) [AddCommGroup M] [Module A M] :
-    SubDPIdeal.generatedDpow (dividedPowers' A M) (ι A M).range = ⊤ := sorry
+--TODO: make this compile
+/- example (A : Type u) [CommRing A] [DecidableEq A] (M : Type u) [AddCommGroup M] [Module A M] :
+    SubDPIdeal.generatedDpow (dividedPowers' A M) (ι A M).range = ⊤ := sorry -/
 
 theorem dp_comp (A : Type u) [CommRing A] [DecidableEq A] (M : Type u) [AddCommGroup M] [Module A M]
     (x : M) {n : ℕ} (m : ℕ) (hn : n ≠ 0) :

DividedPowers/DPAlgebra/Envelope.lean

@@ -37,7 +37,6 @@ theorem IdealAdd.dividedPowers_dpow_eq_algebraMap' (hJ : DividedPowers J)
   rw [← hI'_ext.2 _ ha]
   exact IdealAdd.dpow_eq_of_mem_left _ _ h_int (mem_map_of_mem (algebraMap A B) ha)
 
-  /-∀ {n : ℕ} (a : A), hI'.dpow n ((algebraMap A C) a) = (algebraMap A C) (hI.dpow n a)-/
 
 end IdealAdd
 
@@ -110,7 +109,7 @@ lemma rel1_apply (x : J) :
   rel1 J ((ι B ↥J) x) ((algebraMap B (DividedPowerAlgebra B ↥J)) ↑x) := by constructor
 
 -- J1
-/-- The ideal of the divided power algebra generated by the generators of the first kind 
+/-- The ideal of the divided power algebra generated by the generators of the first kind
 
 [Berthelot-Ogus], page 61, 𝒥₁ -/
 noncomputable def J1 : Ideal (DividedPowerAlgebra B J) :=
@@ -148,7 +147,7 @@ lemma rel2'_apply {x : I} {n : ℕ} (hn : n ≠ 0) :
   rel2'.Rel hn
 
 -- J2
-/-- The ideal of the divided power algebra generated by the generators of the first kind 
+/-- The ideal of the divided power algebra generated by the generators of the first kind
 
 [Berthelot-Ogus], page 61, 𝒥₂ -/
 noncomputable def J2 : Ideal (DividedPowerAlgebra B J) :=
@@ -159,7 +158,7 @@ lemma rel2'_mem_J2 (x : I) {n : ℕ} (hn : n ≠ 0) :
       (ι B J ⟨(algebraMap A B (dpow hI n x)), algebraMap_dpow_mem hI J hIJ x hn⟩) ∈
         J2 hI J hIJ := by
   apply subset_span
-  use (dp B n (⟨algebraMap A B x, hIJ (Ideal.mem_map_of_mem _ x.2)⟩ : J)), 
+  use (dp B n (⟨algebraMap A B x, hIJ (Ideal.mem_map_of_mem _ x.2)⟩ : J)),
       (ι B J ⟨(algebraMap A B (dpow hI n x)), algebraMap_dpow_mem hI J hIJ x hn⟩)
   simp [sub_add_cancel, rel2'_apply hI hIJ hn]
 
@@ -181,17 +180,13 @@ private theorem sub_add_sub {A : Type*} [AddCommGroup A] (a b c d : A) :
 lemma rel2_mem_J12 (x : I) {n : ℕ} (hn : n ≠ 0) :
     (dp B n (⟨algebraMap A B x, hIJ (Ideal.mem_map_of_mem _ x.2)⟩ : J)) -
       algebraMap _ _ (algebraMap A B (dpow hI n x)) ∈ J12 hI J hIJ := by
-  have := rel1_mem_J12 hI J hIJ 
-  have this' := rel1_mem_J12 hI J hIJ (⟨algebraMap A B (dpow hI n x),
+  have h := rel1_mem_J12 hI J hIJ (⟨algebraMap A B (dpow hI n x),
         hIJ (Ideal.mem_map_of_mem (algebraMap A B) (hI.dpow_mem hn x.prop))⟩ : J)
-  rw [← Ideal.neg_mem_iff, neg_sub] at this'
-  rw [← Ideal.add_mem_iff_left (J12 hI J hIJ) this']
-  rw [sub_add_sub]
-  apply Ideal.add_mem
-  · apply mem_sup_right
-    exact rel2'_mem_J2 hI J hIJ x hn
-  · convert zero_mem (J12 hI J hIJ)
-    rw [sub_eq_zero]
+  rw [← Ideal.neg_mem_iff, neg_sub] at h
+  rw [← Ideal.add_mem_iff_left (J12 hI J hIJ) h, sub_add_sub]
+  apply Ideal.add_mem _ (mem_sup_right (rel2'_mem_J2 hI J hIJ x hn))
+  simp only [sub_self, Submodule.zero_mem]
+
 
   /- inductive rel2' : Rel (DividedPowerAlgebra B J) (DividedPowerAlgebra B J)
   | Rel {x : I} {n : ℕ} (hn : n ≠ 0) :
@@ -302,7 +297,7 @@ theorem sub_ideal_dpIdealOfIncluded [DecidableEq B] :
         rw [← neg_sub, Ideal.neg_mem_iff]
         exact rel1_mem_J12 hI J hIJ ⟨y, hyJ⟩
       rw [Submodule.mem_sup]
-      use ((ι B ↥J) ⟨y, hyJ⟩), dp_mem_augIdeal B ↥J zero_lt_one ⟨y, hyJ⟩, 
+      use ((ι B ↥J) ⟨y, hyJ⟩), dp_mem_augIdeal B ↥J zero_lt_one ⟨y, hyJ⟩,
         (((algebraMap B (DividedPowerAlgebra B ↥J)) y) - (ι B ↥J) ⟨y, hyJ⟩), hsub
       rw [← hyx]
       ring
@@ -430,7 +425,7 @@ section General
 
 variable (I)
 
-/-- The modified ideal to build the divided power envelope 
+/-- The modified ideal to build the divided power envelope
 
 [Berthelot-Ogus], page 62, J1 -/
 def J' : Ideal B :=
@@ -450,10 +445,14 @@ def dpEnvelope : Type v :=
 --  DividedPowerAlgebra B (J' I J) ⧸ J12 hI (J' I J) (sub_ideal_J' I J)
 
 noncomputable instance : CommRing (dpEnvelope hI J) :=
-  Ideal.Quotient.commRing _
+  Ideal.Quotient.commRing (J12 hI (J' I J) (sub_ideal_J' I J))
 
 noncomputable instance : Algebra B (dpEnvelope hI J) :=
-  Ideal.Quotient.algebra _
+  Ideal.Quotient.algebra B
+
+lemma algebraMap_eq : algebraMap B (dpEnvelope hI J) =
+    (Ideal.Quotient.mk (J12 hI (J' I J) (sub_ideal_J' I J))).comp
+      (algebraMap B (DividedPowerAlgebra B (J' I J))) := rfl
 
 noncomputable instance algebra' : Algebra A (dpEnvelope hI J) :=
   ((algebraMap B (dpEnvelope hI J)).comp (algebraMap A B)).toAlgebra
@@ -499,7 +498,7 @@ noncomputable def dpIdeal' : (dividedPowers' B ↥(J' I J)).SubDPIdeal :=
 
 
 lemma J_le_J₁_bar : map (algebraMap B (dpEnvelope hI J)) J ≤ J₁_bar hI J :=
-  le_trans (map_mono (le_sup_of_le_left (le_refl J))) 
+  le_trans (map_mono (le_sup_of_le_left (le_refl J)))
     (sub_ideal_dpIdealOfIncluded hI (J' I J) (sub_ideal_J' I J))
 
 /-- The divided power ideal of the divided power envelope
@@ -521,37 +520,6 @@ noncomputable def dividedPowers [∀ x, Decidable (x ∈  (dpIdeal hI J).carrier
     DividedPowers (dpIdeal hI J).carrier :=
   IsSubDPIdeal.dividedPowers (dividedPowers' hI J) (dpIdeal hI J).toIsSubDPIdeal
 
--- I am not sure this is the right approach
--- Need compatibility btw I, ker f
--- x ∈ I ∩ ker f, dpow n x ∈ ker f (for n > 0)
-/- noncomputable def dividedPowers_of_map {C : Type*} [CommRing C] (f : A →+* C)
-    [∀ c, Decidable (c ∈ map f I)] : DividedPowers (I.map f) where
-  dpow      := fun n c ↦
-    if hc : c ∈ I.map f then by
-      rw [Ideal.map, span, mem_span_set'] at hc
-      set m := hc.choose with hm
-      set fn := hc.choose_spec.choose with hfn
-      set g := hc.choose_spec.choose_spec.choose with hg
-      let hgc := hc.choose_spec.choose_spec.choose_spec
-      rw [← hg, ← hfn] at hgc
-      have hgi : ∀ i : Fin hc.choose, ∃ a : A, f a = g i := sorry
-/-       let foo := (Finset.sym (Set.univ : Set (Fin hc.choose)) n).sum fun k =>
-        (Set.univ : Set (Fin hc.choose)).prod fun i => hI.dpow (Multiset.count i k) (hgi i).choose-/
-      sorry
-    else 0
-  dpow_null hc := by simp only [dif_neg hc]
-  dpow_zero := by
-    intro c hc
-    simp only [dif_pos hc]
-    --simp_rw [dpow_zero]
-    sorry
-  dpow_one  := sorry
-  dpow_mem  := sorry
-  dpow_add  := sorry
-  dpow_smul := sorry
-  dpow_mul  := sorry
-  dpow_comp := sorry -/
-
 -- Second part of Theorem 3.19
 lemma isCompatibleWith [∀ x, Decidable (x ∈ (dpIdeal hI J).carrier)] :
     IsCompatibleWith hI (dividedPowers hI J) (algebraMap A (dpEnvelope hI J)) := by
@@ -561,16 +529,31 @@ lemma isCompatibleWith [∀ x, Decidable (x ∈ (dpIdeal hI J).carrier)] :
 end DecidableEq
 section
 
-lemma map_generatedDpow_le_of_subDPIdeal
-    {A B : Type*} [CommRing A] [CommRing B] {I : Ideal A} {hI : DividedPowers I}
-    {J : Ideal B} {hJ : DividedPowers J} {J' : SubDPIdeal hJ}
-    {φ : DPMorphism hI hJ} {s : Set A} (hs : s ⊆ I) (hφs : φ '' s ⊆ J') : 
+lemma map_generatedDpow_le {A B : Type*} [CommRing A] [CommRing B] {I : Ideal A}
+    {hI : DividedPowers I} {J : Ideal B} {hJ : DividedPowers J}
+    (φ : DPMorphism hI hJ) {s : Set A} (hs : s ⊆ I)  :
+    (SubDPIdeal.generatedDpow hI hs).carrier.map φ.toRingHom ≤ J := by
+  simp only [SubDPIdeal.generatedDpow_carrier, map_span, span_le]
+  rintro _ ⟨_, ⟨⟨n, hn, x, hx, rfl⟩, rfl⟩⟩
+  rw [← φ.dpow_comp (n := n) x (hs hx)]
+  exact hJ.dpow_mem hn (φ.ideal_comp (Ideal.mem_map_of_mem _ (hs hx)))
+
+lemma map_generatedDpow_le_of_subDPIdeal {A B : Type*} [CommRing A] [CommRing B] {I : Ideal A}
+    {hI : DividedPowers I} {J : Ideal B} {hJ : DividedPowers J} {J' : SubDPIdeal hJ}
+    {φ : DPMorphism hI hJ} {s : Set A} (hs : s ⊆ I) (hφs : φ '' s ⊆ J') :
     (SubDPIdeal.generatedDpow hI hs).carrier.map φ.toRingHom ≤ J'.carrier := by
   simp only [SubDPIdeal.generatedDpow_carrier, map_span, span_le]
   rintro _ ⟨_, ⟨⟨n, hn, x, hx, rfl⟩, rfl⟩⟩
   rw [← φ.dpow_comp (n := n) x (hs hx)]
   exact J'.dpow_mem hn (φ x) (hφs (Set.mem_image_of_mem (⇑φ) hx))
 
+-- Needed because `DPEnvelope` and `DPEnvelopeOfIncluded` are not the same type.
+variable {hI J} in
+theorem mem_dpIdealOfIncluded_of_mem_dpIdeal [DecidableEq B] {a : dpEnvelope hI J}
+    (ha : a ∈ (dpIdeal hI J)) : a ∈ dpIdealOfIncluded hI (J' I J) (sub_ideal_J' I J) :=
+  map_generatedDpow_le (DPMorphism.id (dividedPowers' hI J) ) (J_le_J₁_bar hI J)
+    (Ideal.mem_map_of_mem _ ha)
+
 -- Universal property claim of Theorem 3.19
 theorem dpEnvelope_IsDPEnvelope [DecidableEq B] [∀ x, Decidable (x ∈  (dpIdeal hI J).carrier)] :
     IsDPEnvelope hI J (dpIdeal hI J) (dividedPowers hI J)
@@ -603,13 +586,7 @@ theorem dpEnvelope_IsDPEnvelope [DecidableEq B] [∀ x, Decidable (x ∈  (dpIde
     simp only [J', Submodule.add_eq_sup, Ideal.map_sup, Ideal.map_map,
       ← IsScalarTower.algebraMap_eq]
     exact le_sup_of_le_right (le_refl _)
-  /- Q: I am trying to follow "The General Case" section in page 63 of B-O. If I understand
-    correctly, what they are saying is that the map `φ` above is also a DP morphism from
-    `dpIdeal hI J` to `K`, because the image of `dpIdeal hI J` is contained in `K`. However I
-    cannot prove this (see line 609). -/
-  /- A: In fact, you applied a too harsh le_trans at the beginning of the proof.
-        I have to admit that the indications of [Berthelot-Ogus] are very terse.
-        The difficulty of this formalization also proves its necessity… -/
+  have := φ.ideal_comp
   set K' : SubDPIdeal h1 :=
     { carrier := K
       isSubideal := le_sup_right
@@ -631,57 +608,25 @@ theorem dpEnvelope_IsDPEnvelope [DecidableEq B] [∀ x, Decidable (x ∈  (dpIde
         simp only [dpEnvelope, hφ, SetLike.mem_coe]
         apply le_trans hJK (le_refl K)
         exact mem_map_of_mem (algebraMap B C) hb
-        /-
-        apply le_trans _
-          (SubDPIdeal.generated_dpow_le hK (map (algebraMap B C) J) (⊤ : hK.SubDPIdeal) hJK)
-        simp only [dpIdeal, SubDPIdeal.generatedDpow, SetLike.mem_coe, exists_prop', nonempty_prop,
-          ne_eq, Nat.exists_ne_zero, Ideal.map_span]
-        apply Ideal.span_mono
-        intro x hx
-        simp only [Set.mem_image, Set.mem_setOf_eq] at hx
-        obtain ⟨y, ⟨n, ⟨x, hx, rfl⟩⟩, rfl⟩ := hx
-        simp only [Set.mem_setOf_eq]
-        use n, φ.toRingHom x
-        constructor
-        · rw [← hφ, ← Ideal.map_map]
-          exact Ideal.mem_map_of_mem _ hx
-        · have hK1 : hK.dpow (n + 1) (φ.toRingHom x) = h1.dpow (n + 1) (φ.toRingHom x) := by
-            simp only [h1_def]
-            rw [← IdealAdd.dpow_eq_of_mem_right hI' hK hI'_int]
-            · rfl
-            have hxK : φ.toRingHom x ∈ map φ.toRingHom (map (algebraMap B (dpEnvelope hI J)) J) :=
-              Ideal.mem_map_of_mem _ hx
-            simp only [Ideal.map_map] at hxK
-            apply hJK
-            rw [← hφ]
-            exact hxK
-          rw [hK1, φ.dpow_comp]
-          · rfl
-          · simp only [dpIdealOfIncluded]
-            apply Set.mem_of_subset_of_mem _ hx
-            simp only [SetLike.coe_subset_coe]
-            have heq : algebraMap B (dpEnvelope hI J) =
-             (algebraMap (DividedPowerAlgebra B ↥(J' I J)) (dpEnvelope hI J)).comp
-             (algebraMap B (DividedPowerAlgebra B ↥(J' I J))) := by rfl
-            rw [heq, ← Ideal.map_map]
-            apply Ideal.map_mono
-            intro x hx
-            simp only [map] at hx
-            -- Q (follow up from line 567): this seems false, which would suggest that the proof
-            -- strategy from B-O does not work.
-            sorry -/
       dpow_comp  := fun {n} a ha => by
         -- On `K`, `h1.dpow` coincides with `hK.dpow`, by `dpow_eq_of_mem_right`
         -- The left hand side applies to `φ a`, so `hK` can be changed to `h1`
-        -- Then apply the property of `φ`
-        -- Get `dpow` for `dpEnvelopeOfIncluded`, for `J' I J`, 
-        -- but this will be the same as `dpow` for `dpEnvelope` because the element is there.
-        -- 
-        --have := φ.dpow_comp
-        -- obtain ⟨r, s⟩ := hI1
-        --rw ← hI'_ext,
-        --rw φ.dpow_comp,
-        sorry }
+        rw [← IdealAdd.dpow_eq_of_mem_right hI' hK hI'_int ]
+        · have hφ_comp : ∀ {n : ℕ}, ∀ a ∈ _, h1.dpow n (φ a) = φ _ := φ.dpow_comp
+          have ha' : a ∈ dpIdealOfIncluded hI (J' I J) (sub_ideal_J' I J) :=
+            mem_dpIdealOfIncluded_of_mem_dpIdeal ha
+          have h1_dpow : IdealAdd.dpow hI' hK n (φ.toRingHom a) = h1 n (φ a) := rfl
+          -- Then we apply `φ.dpow_comp`
+          erw [h1_dpow, hφ_comp (n := n) a ha']
+          change _ = φ ((dividedPowers hI J).dpow n a)
+          congr 1
+          -- Get `dpow` for `dpEnvelopeOfIncluded`, for `J' I J`,
+          -- but this will be the same as `dpow` for `dpEnvelope` because the element is there.
+          rw [dividedPowers, IsSubDPIdeal.dpow_eq, if_pos ha]
+          rfl
+        · -- φ.toRingHom a ∈ K
+          sorry
+ }
   use ψ
   refine ⟨by rw [← hφ]; rfl, ?_⟩
   intro α hα
@@ -702,7 +647,8 @@ theorem dpEnvelope_IsDPEnvelope [DecidableEq B] [∀ x, Decidable (x ∈  (dpIde
       -- and it is basically obvious that they map to `K1`
       -- But, the elements of `J` map to `K` (hypothesis)
       -- and the elements of `I` map to `K` as well (another hypothesis)
-      apply le_trans _ α.ideal_comp
+      sorry
+      /- apply le_trans _ α.ideal_comp
       apply Ideal.map_mono
       intro x hx
       simp only [SubDPIdeal.memCarrier, dpIdeal, SubDPIdeal.generatedDpow]
@@ -717,7 +663,7 @@ theorem dpEnvelope_IsDPEnvelope [DecidableEq B] [∀ x, Decidable (x ∈  (dpIde
       · intro a _ b _ ha hb
         exact Ideal.add_mem _ ha hb
       · intro a x _ hx
-        exact Submodule.smul_mem _ a hx
+        exact Submodule.smul_mem _ a hx -/
     dpow_comp  := fun a ha => by
       obtain ⟨hK', hmap, hint⟩ := hI1
       --rw [← hα] at hmapc

DividedPowers/DPAlgebra/Graded/GradeZero.lean

@@ -207,7 +207,7 @@ theorem coeff_zero_of_mem_augIdeal {f : MvPolynomial (ℕ × M) R}
     rw [monomial_zero', aeval_C, Algebra.id.map_eq_id, RingHom.id_apply, ←
       not_mem_support_iff.mp hf']
 
-theorem  augIdeal_eq_span :
+theorem augIdeal_eq_span :
     augIdeal R M = span (Set.image2 (dp R) {n : ℕ | 0 < n} Set.univ) := by
   classical
   apply le_antisymm