From 12904db83fd79f11471b2e515ae55e524e94e237 Mon Sep 17 00:00:00 2001 From: mariainesdff Date: Fri, 20 Dec 2024 13:15:42 +0100 Subject: [PATCH] progress on dpow_comp --- DividedPowers/DPAlgebra/Dpow.lean | 5 +- DividedPowers/DPAlgebra/Envelope.lean | 168 ++++++------------ DividedPowers/DPAlgebra/Graded/GradeZero.lean | 2 +- 3 files changed, 61 insertions(+), 114 deletions(-) diff --git a/DividedPowers/DPAlgebra/Dpow.lean b/DividedPowers/DPAlgebra/Dpow.lean index e6c3931..d8f67b3 100644 --- a/DividedPowers/DPAlgebra/Dpow.lean +++ b/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) : diff --git a/DividedPowers/DPAlgebra/Envelope.lean b/DividedPowers/DPAlgebra/Envelope.lean index d6d0ee3..8673bd9 100644 --- a/DividedPowers/DPAlgebra/Envelope.lean +++ b/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 diff --git a/DividedPowers/DPAlgebra/Graded/GradeZero.lean b/DividedPowers/DPAlgebra/Graded/GradeZero.lean index 49e3b34..4531d2b 100644 --- a/DividedPowers/DPAlgebra/Graded/GradeZero.lean +++ b/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