rename isSubDPIdeal, golf

AntoineChambert-Loir · Oct 16, 2024 · 4f4f886 · 4f4f886
1 parent c7e0882
commit 4f4f886
Show file tree

Hide file tree

Showing 3 changed files with 287 additions and 371 deletions.
diff --git a/DividedPowers/DPAlgebra/Compatible.lean b/DividedPowers/DPAlgebra/Compatible.lean
@@ -11,6 +11,11 @@ def extends_to {A : Type u} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B
     [CommRing B] (f : A →+* B) : Prop :=
   ∃ hI' : DividedPowers (I.map f), isDPMorphism hI hI' f
 
+/- lemma extends_to_def {A : Type u} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type v}
+    [CommRing B] (f : A →+* B) :
+    extends_to hI f ↔ ∃ hI' : DividedPowers (I.map f), isDPMorphism hI hI' f :=
+  by simp only [extends_to] -/
+
 lemma isDPMorphism.span_map_le {A : Type u} [CommRing A] {I : Ideal A} (hI : DividedPowers I)
     {B : Type v} [CommRing B] (f : A →+* B) (K : Ideal B) (hK : DividedPowers K)
       (hIKf : isDPMorphism hI hK f) :
@@ -56,11 +61,11 @@ lemma extends_to_iff_exists_dpIdeal {A : Type u} [CommRing A] {I : Ideal A} (hI
     extends_to hI f ↔ ∃ (J : Ideal B) (hJ : DividedPowers J), isDPMorphism hI hJ f := by
   classical
   refine ⟨fun ⟨hJ, hmap⟩ ↦ ⟨I.map f, hJ, hmap⟩, fun ⟨J, hJ, hmap⟩ ↦  ?_⟩
-  use (isSubDPIdeal_map _ _ hmap).dividedPowers
+  use (IsSubDPIdeal_map _ _ hmap).dividedPowers
   rw [isDPMorphism] at hmap ⊢
   refine ⟨le_refl _, ?_⟩
   intros n a ha
-  rw [isSubDPIdeal.dividedPowers.dpow_eq, if_pos (I.mem_map_of_mem f ha), hmap.2 n a ha]
+  rw [IsSubDPIdeal.dividedPowers.dpow_eq, if_pos (I.mem_map_of_mem f ha), hmap.2 n a ha]
 
 -- Note (3) after 3.14: in general the extension does not exist.
 
@@ -184,10 +189,10 @@ lemma extends_to_of_principal {J : Ideal A} (hJ : DividedPowers J) (hJp : Submod
 
 end IsPrincipal
 
-lemma isDPMorphism.isSubDPIdeal_map {A : Type u} [CommRing A] {I : Ideal A} (hI : DividedPowers I)
+lemma isDPMorphism.IsSubDPIdeal_map {A : Type u} [CommRing A] {I : Ideal A} (hI : DividedPowers I)
     {B : Type v} [CommRing B] (f : A →+* B) {K : Ideal B} (hK : DividedPowers K)
     (hIK : isDPMorphism hI hK f) :
-    isSubDPIdeal hK (I.map f) := {
+    IsSubDPIdeal hK (I.map f) := {
       isSubIdeal := hIK.1
       dpow_mem   := by
         have hsub : Submodule.span B (f '' I) ≤ K := by
@@ -246,19 +251,19 @@ lemma IsCompatibleWith_tfae {A : Type u} [CommRing A] {I : Ideal A} (hI : Divide
     use I.map f + J, le_refl _, hK
   tfae_have 3 → 1
   · rintro ⟨K, hIJK, hK, hIK, hJK⟩
-    have hsub : isSubDPIdeal hK (I.map f) := isDPMorphism.isSubDPIdeal_map hI f hK hIK
-    set hK' : DividedPowers (map f I) := isSubDPIdeal.dividedPowers hK hsub
+    have hsub : IsSubDPIdeal hK (I.map f) := isDPMorphism.IsSubDPIdeal_map hI f hK hIK
+    set hK' : DividedPowers (map f I) := IsSubDPIdeal.dividedPowers hK hsub
     use hK'
     constructor
     · simp only [isDPMorphism, le_refl, true_and]
       intro n a ha
-      -- we need some API to use isSubDPIdeal.dividedPowers
-      simp only [hK', isSubDPIdeal.dividedPowers]
+      -- we need some API to use IsSubDPIdeal.dividedPowers
+      simp only [hK', IsSubDPIdeal.dividedPowers]
       rw [if_pos (Ideal.mem_map_of_mem f ha), hIK.map_dpow n a ha]
     · rintro n b ⟨hb , hb'⟩
       simp only [SetLike.mem_coe] at hb hb'
-      -- we need some API to use isSubDPIdeal.dividedPowers
-      simp only [hK', isSubDPIdeal.dividedPowers]
+      -- we need some API to use IsSubDPIdeal.dividedPowers
+      simp only [hK', IsSubDPIdeal.dividedPowers]
       rw [if_pos hb', show hJ.dpow n b = hK.dpow n b by
         simpa only [RingHom.id_apply] using hJK.map_dpow n b hb]
   tfae_finish
@@ -268,8 +273,8 @@ lemma IsCompatibleWith_tfae {A : Type u} [CommRing A] {I : Ideal A} (hI : Divide
 /-- B-0 Def 3.17 (using condition 1 of Prop. 3.16) -/
 def IsCompatibleWith {A : Type u} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {B : Type v}
     [CommRing B] {J : Ideal B} (hJ : DividedPowers J) (f : A →+* B) : Prop :=
-  ∃ hI' : DividedPowers (I.map f),
-    (∀ (n : ℕ) (a : A), hI'.dpow n (f a) = f (hI.dpow n a)) ∧
-      ∀ (n : ℕ) (b : B) (_ : b ∈ J ⊓ I.map f), hJ.dpow n b = hI'.dpow n b
+  ∃ hI' : DividedPowers (I.map f), isDPMorphism hI hI' f
+    /- (∀ (n : ℕ) (a : A), hI'.dpow n (f a) = f (hI.dpow n a)) -/ ∧
+      ∀ (n : ℕ) (b : B) (_ : b ∈ J ⊓ I.map f),  hI'.dpow n b = hJ.dpow n b
 
 end DividedPowers
diff --git a/DividedPowers/DPAlgebra/Dpow.lean b/DividedPowers/DPAlgebra/Dpow.lean
@@ -612,11 +612,11 @@ example (A : Type u) [CommRing A] {R S R' S' : Type u} [CommRing R] [CommRing S]
       ext x
       simp only [RingHom.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
         Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.map_tmul, map_one]
-  have hK'_pd : isSubDPIdeal hK (RingHom.ker fg ⊓ K A I J) := by
+  have hK'_pd : IsSubDPIdeal hK (RingHom.ker fg ⊓ K A I J) := by
     rw [roby]
-    apply isSubDPIdeal_sup
-    exact isSubDPIdeal_map_of_isSubDPIdeal hI hK hK_pd.1 _ (isSubDPIdeal_ker hI hI' hf')
-    exact isSubDPIdeal_map_of_isSubDPIdeal hJ hK hK_pd.2 _ (isSubDPIdeal_ker hJ hJ' hg')
+    exact IsSubDPIdeal_sup _
+      (IsSubDPIdeal_map_of_IsSubDPIdeal hI hK hK_pd.1 (IsSubDPIdeal_ker hI hI' hf'))
+      (IsSubDPIdeal_map_of_IsSubDPIdeal hJ hK hK_pd.2 (IsSubDPIdeal_ker hJ hJ' hg'))
   rw [hK_map]
   use DividedPowers.Quotient.OfSurjective.dividedPowers hK s_fg hK'_pd
   constructor
@@ -766,7 +766,7 @@ theorem condτ_rel (A : Type u) [CommRing A]
       ext x
       simp only [RingHom.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
         Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.map_tmul, map_one]
-  have hK'_pd : isSubDPIdeal hK (RingHom.ker fg ⊓ K A I J) := by
+  have hK'_pd : IsSubDPIdeal hK (RingHom.ker fg ⊓ K A I J) := by
     have := Algebra.TensorProduct.map_ker _ _ hf hg
     have hkerf := RingHom.ker_eq_span_union A R R₀ I
       ((Ideal.isAugmentation_subalgebra_iff A).mp hR₀I).codisjoint
@@ -790,7 +790,7 @@ theorem condτ_rel (A : Type u) [CommRing A]
     rw [sup_sup_sup_comm] at this
     simp only [Ideal.map_span] at this
     rw [this]
-    -- we need a variant of `isSubDPIdeal_sup`
+    -- we need a variant of `IsSubDPIdeal_sup`
     suffices this :
       ((span (Algebra.TensorProduct.includeLeft (R := A) (S := A) (A := R) (B := S) ''
         (↑(RingHom.ker f) ∩ (R₀ : Set R))) ⊔
@@ -802,13 +802,13 @@ theorem condτ_rel (A : Type u) [CommRing A]
         span (⇑Algebra.TensorProduct.includeRight '' (↑(RingHom.ker g) ∩ ↑J)))) by
       rw [this]
       simp only [← Ideal.map_span]
-      apply isSubDPIdeal_sup
+      apply IsSubDPIdeal_sup
       · have : span (↑(RingHom.ker f) ∩ ↑I) = RingHom.ker f ⊓ I := sorry
         rw [this]
-        exact isSubDPIdeal_map_of_isSubDPIdeal hI hK hK_pd.1 _ (isSubDPIdeal_ker hI hI' hfDP)
+        exact IsSubDPIdeal_map_of_IsSubDPIdeal hI hK hK_pd.1 (IsSubDPIdeal_ker hI hI' hfDP)
       · have : span (↑(RingHom.ker g) ∩ ↑J) = RingHom.ker g ⊓ J := sorry
         rw [this]
-        exact isSubDPIdeal_map_of_isSubDPIdeal hJ hK hK_pd.2 _ (isSubDPIdeal_ker hJ hJ' hgDP)
+        exact IsSubDPIdeal_map_of_IsSubDPIdeal hJ hK hK_pd.2 (IsSubDPIdeal_ker hJ hJ' hgDP)
     sorry
   rw [hK_map]
   use DividedPowers.Quotient.OfSurjective.dividedPowers hK s_fg hK'_pd
@@ -998,7 +998,7 @@ theorem roby_prop_4
     {R₀ : Subalgebra A R} (hsplit : IsAugmentation R₀ I) (hI : DividedPowers I) {J : Ideal R}
     {F₀ : Set R₀} {FI : Set I}
     (hJ : J = Submodule.span R ((R₀.val '' F₀) ∪ (I.subtype '' FI) : Set R)) :
-    hI.isSubDPIdeal (J ⊓ I) ↔ (∀ a ∈ FI, ∀ n ≠ 0, hI.dpow n a ∈ J):= by
+    hI.IsSubDPIdeal (J ⊓ I) ↔ (∀ a ∈ FI, ∀ n ≠ 0, hI.dpow n a ∈ J):= by
   simp only [Ideal.isAugmentation_subalgebra_iff] at hsplit
   constructor
   · intro hJ'