diff --git a/DividedPowers/DPAlgebra/Dpow.lean b/DividedPowers/DPAlgebra/Dpow.lean index 17309dc..9fd263b 100644 --- a/DividedPowers/DPAlgebra/Dpow.lean +++ b/DividedPowers/DPAlgebra/Dpow.lean @@ -998,7 +998,7 @@ theorem roby_prop_4 apply inf_le_right (a := J) simp only [ge_iff_le, le_refl, inf_of_le_left] apply inf_le_left (b := I) - apply hJ'.dpow_mem n hn + apply hJ'.dpow_mem hn simp only [Ideal.mem_inf, SetLike.coe_mem, and_true] exact hJ ▸ subset_span (Set.mem_union_right _ ⟨a, ha, rfl⟩) · intro H @@ -1034,10 +1034,10 @@ theorem roby_prop_4 exact inf_le_right (a := J) (hT_le hx) suffices T = J ⊓ I by exact { isSubideal := inf_le_right - dpow_mem := fun n hn a ha ↦ by + dpow_mem := fun hn a ha ↦ by simp only [Ideal.mem_inf] at ha ⊢ suffices ha' : a ∈ T by - exact ⟨ha'.2 n hn, hI.dpow_mem hn ha.2⟩ + exact ⟨ha'.2 _ hn, hI.dpow_mem hn ha.2⟩ simp only [this, Submodule.inf_coe, Set.mem_inter_iff, SetLike.mem_coe, ha.2, ha.1, and_true] } set U := (J.restrictScalars A ⊓ Subalgebra.toSubmodule R₀) ⊔ (Ideal.span T).restrictScalars A with hU diff --git a/DividedPowers/DPAlgebra/Envelope.lean b/DividedPowers/DPAlgebra/Envelope.lean index 8b39200..82a5820 100644 --- a/DividedPowers/DPAlgebra/Envelope.lean +++ b/DividedPowers/DPAlgebra/Envelope.lean @@ -160,7 +160,7 @@ theorem J12_IsSubDPIdeal [DecidableEq B] : IsSubDPIdeal (DividedPowerAlgebra.dividedPowers' B J) (J12 hI J hIJ ⊓ DividedPowerAlgebra.augIdeal B J) where isSubideal := inf_le_right - dpow_mem := fun n hn x hx ↦ by + dpow_mem := fun hn x hx ↦ by have hJ12 : J12 hI J hIJ ⊓ augIdeal B J = (J1 J ⊓ augIdeal B J) + J2 hI J hIJ := sorry --simp only [dividedPowers', Subtype.forall, mem_inf] rw [hJ12, Submodule.add_eq_sup, Submodule.mem_sup'] at hx @@ -184,7 +184,7 @@ theorem J12_IsSubDPIdeal [DecidableEq B] : have hss : J1 J * augIdeal B ↥J ≤ J12 hI J hIJ ⊓ augIdeal B ↥J := heq ▸ inf_le_inf_right (augIdeal B ↥J) le_sup_left rw [heq] at hx1 - exact hss (hsub.dpow_mem n hn hx1) + exact hss (hsub.dpow_mem hn hx1) · sorry/- revert n induction x2 using DividedPowerAlgebra.induction_on with | h_C b => diff --git a/DividedPowers/IdealAdd.lean b/DividedPowers/IdealAdd.lean index 676e5c3..cecb90e 100644 --- a/DividedPowers/IdealAdd.lean +++ b/DividedPowers/IdealAdd.lean @@ -503,11 +503,11 @@ theorem dpow_unique (hsup : DividedPowers (I + J)) lemma isDPMorphism_left (hIJ : ∀ {n : ℕ}, ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a) : hI.IsDPMorphism (IdealAdd.dividedPowers hI hJ hIJ) (RingHom.id A):= - ⟨by simp only [Ideal.map_id]; exact le_sup_left, fun _ ha ↦ dpow_eq_of_mem_left hI hJ hIJ ha⟩ + ⟨by simp only [Ideal.map_id]; exact le_sup_left, fun _ ↦ dpow_eq_of_mem_left hI hJ hIJ⟩ lemma isDPMorphism_right (hIJ : ∀ {n : ℕ}, ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a) : hJ.IsDPMorphism (IdealAdd.dividedPowers hI hJ hIJ) (RingHom.id A) := - ⟨by simp only [Ideal.map_id]; exact le_sup_right, fun _ ha ↦ dpow_eq_of_mem_right hI hJ hIJ ha⟩ + ⟨by simp only [Ideal.map_id]; exact le_sup_right, fun _ ↦ dpow_eq_of_mem_right hI hJ hIJ⟩ end IdealAdd diff --git a/DividedPowers/RatAlgebra.lean b/DividedPowers/RatAlgebra.lean index f8e254c..a3e90c0 100644 --- a/DividedPowers/RatAlgebra.lean +++ b/DividedPowers/RatAlgebra.lean @@ -227,7 +227,7 @@ namespace RatAlgebra variable {R : Type*} [CommSemiring R] (I : Ideal R) [DecidablePred (fun x ↦ x ∈ I)] /-- The family `ℕ → R → R` given by `dpow n x = x ^ n / n!`. -/ -noncomputable def dpow : ℕ → R → R := fun n => OfInvertibleFactorial.dpow I n +noncomputable def dpow : ℕ → R → R := OfInvertibleFactorial.dpow I variable {I} @@ -263,7 +263,7 @@ omit [DecidablePred fun x ↦ x ∈ I] in /-- If `I` is an ideal in a `ℚ`-algebra `A`, then the divided power structure on `I` given by `dpow n x = x ^ n / n!` is the only possible one. -/ theorem dpow_eq_inv_fact_smul (hI : DividedPowers I) {n : ℕ} {x : R} (hx : x ∈ I) : - hI.dpow n x = (inverse (Nat.factorial n : ℚ) : ℚ) • x ^ n := by + hI.dpow n x = (inverse (n.factorial : ℚ)) • x ^ n := by rw [inverse_eq_inv', ← factorial_mul_dpow_eq_pow hI hx, ← smul_eq_mul, ← smul_assoc] nth_rewrite 1 [← one_smul R (hI.dpow n x)] congr diff --git a/DividedPowers/SubDPIdeal.lean b/DividedPowers/SubDPIdeal.lean index 1b38f2e..2c50355 100644 --- a/DividedPowers/SubDPIdeal.lean +++ b/DividedPowers/SubDPIdeal.lean @@ -70,7 +70,7 @@ namespace DividedPowers structure IsSubDPIdeal {A : Type*} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) (J : Ideal A) : Prop where isSubideal : J ≤ I - dpow_mem : ∀ (n : ℕ) (_: n ≠ 0) {j : A} (_ : j ∈ J), hI.dpow n j ∈ J + dpow_mem : ∀ {n : ℕ} (_: n ≠ 0) {j : A} (_ : j ∈ J), hI.dpow n j ∈ J section IsSubDPIdeal namespace IsSubDPIdeal @@ -81,7 +81,7 @@ open Ideal theorem self : IsSubDPIdeal hI I where isSubideal := le_rfl - dpow_mem _ hn _ ha := hI.dpow_mem hn ha + dpow_mem hn _ ha := hI.dpow_mem hn ha def dividedPowers {J : Ideal A} (hJ : IsSubDPIdeal hI J) [∀ x, Decidable (x ∈ J)] : DividedPowers J where @@ -89,14 +89,14 @@ def dividedPowers {J : Ideal A} (hJ : IsSubDPIdeal hI J) [∀ x, Decidable (x dpow_null hx := by simp only [if_neg hx] dpow_zero hx := by simp only [if_pos hx, hI.dpow_zero (hJ.isSubideal hx)] dpow_one hx := by simp only [if_pos hx, hI.dpow_one (hJ.isSubideal hx)] - dpow_mem hn hx := by simp only [if_pos hx, hJ.dpow_mem _ hn hx] + dpow_mem hn hx := by simp only [if_pos hx, hJ.dpow_mem hn hx] dpow_add hx hy := by simp_rw [if_pos hx, if_pos hy, if_pos (Ideal.add_mem J hx hy), hI.dpow_add (hJ.isSubideal hx) (hJ.isSubideal hy)] dpow_smul hx := by simp only [if_pos hx, if_pos (mul_mem_left J _ hx), hI.dpow_smul (hJ.isSubideal hx)] dpow_mul hx := by simp only [if_pos hx, hI.dpow_mul (hJ.isSubideal hx)] dpow_comp hn hx := by - simp only [if_pos hx, if_pos (hJ.dpow_mem _ hn hx), hI.dpow_comp hn (hJ.isSubideal hx)] + simp only [if_pos hx, if_pos (hJ.dpow_mem hn hx), hI.dpow_comp hn (hJ.isSubideal hx)] variable {J : Ideal A} (hJ : IsSubDPIdeal hI J) [∀ x, Decidable (x ∈ J)] @@ -110,7 +110,7 @@ end IsSubDPIdeal open Finset Ideal -/-- The ideal `J ⊓ I` is a sub-dp-ideal of `I` if and only if (on `I`) the divided powers have +/-- The ideal `J ⊓ I` is a sub-dp-ideal of `I` if and only if (on `I`) the divided powers have some compatiblity mod `J`. (The necessity was proved as a sanity check.) -/ theorem IsSubDPIdeal_inf_iff {A : Type*} [CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} : IsSubDPIdeal hI (J ⊓ I) ↔ @@ -120,7 +120,7 @@ theorem IsSubDPIdeal_inf_iff {A : Type*} [CommRing A] {I : Ideal A} (hI : Divide rw [← add_sub_cancel b a, hI.dpow_add' hb hab', range_succ, sum_insert not_mem_range_self, tsub_self, hI.dpow_zero hab', mul_one,add_sub_cancel_left] exact J.sum_mem (fun i hi ↦ SemilatticeInf.inf_le_left J I ((J ⊓ I).smul_mem _ - (hIJ.dpow_mem _ (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩))) + (hIJ.dpow_mem (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩))) · refine ⟨SemilatticeInf.inf_le_right J I, fun {n} hn {a} ha ↦ ⟨?_, hI.dpow_mem hn ha.right⟩⟩ rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn] exact hIJ n a 0 ha.right I.zero_mem (J.sub_mem ha.left J.zero_mem) @@ -130,32 +130,35 @@ variable {A B : Type*} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J /-- Lemma 3.6 of [BO] (Antoine) -/ theorem span_IsSubDPIdeal_iff (S : Set A) (hS : S ⊆ I) : - IsSubDPIdeal hI (span S) ↔ ∀ (n : ℕ) (_ : n ≠ 0), ∀ s ∈ S, hI.dpow n s ∈ span S := by - refine ⟨fun hhI n hn s hs ↦ hhI.dpow_mem _ hn (subset_span hs), ?_⟩ + IsSubDPIdeal hI (span S) ↔ ∀ {n : ℕ} (_ : n ≠ 0), ∀ s ∈ S, hI.dpow n s ∈ span S := by + refine ⟨fun hhI n hn s hs ↦ hhI.dpow_mem hn (subset_span hs), ?_⟩ · -- interesting direction, intro hhI have hSI := span_le.mpr hS apply IsSubDPIdeal.mk hSI - intro n hn z hz; revert n - refine Submodule.span_induction' ?_ ?_ ?_ ?_ hz - ·-- case of elements of S - exact fun s hs n hn ↦ hhI n hn s hs - ·-- case of 0 - intro _ hn - rw [hI.dpow_eval_zero hn] - exact (span S).zero_mem - · -- case of sum - intro x hxI y hyI hx hy n hn - rw [hI.dpow_add' (hSI hxI) (hSI hyI)] - apply Submodule.sum_mem (span S) - intro m _ - by_cases hm0 : m = 0 - · exact hm0 ▸ mul_mem_left (span S) _ (hy _ hn) - · exact mul_mem_right _ (span S) (hx _ hm0) - · -- case : product, - intro a x hxI hx n hn - rw [Algebra.id.smul_eq_mul, hI.dpow_smul (hSI hxI)] - exact mul_mem_left (span S) (a ^ n) (hx n hn) + intro m hm z hz + -- This solution is a bit hacky, but it works... + have haux : ∀ (n : ℕ), n ≠ 0 → hI.dpow n z ∈ span S := by + refine Submodule.span_induction' ?_ ?_ ?_ ?_ hz + ·-- case of elements of S + exact fun s hs n hn ↦ hhI hn s hs + ·-- case of 0 + intro _ hn + rw [hI.dpow_eval_zero hn] + exact (span S).zero_mem + · -- case of sum + intro x hxI y hyI hx hy n hn + rw [hI.dpow_add' (hSI hxI) (hSI hyI)] + apply Submodule.sum_mem (span S) + intro m _ + by_cases hm0 : m = 0 + · exact hm0 ▸ mul_mem_left (span S) _ (hy _ hn) + · exact mul_mem_right _ (span S) (hx _ hm0) + · -- case : product, + intro a x hxI hx n hn + rw [Algebra.id.smul_eq_mul, hI.dpow_smul (hSI hxI)] + exact mul_mem_left (span S) (a ^ n) (hx n hn) + exact @haux m hm theorem generated_dpow_isSubideal {S : Set A} (hS : S ⊆ I) : span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I := by @@ -169,21 +172,21 @@ theorem IsSubDPIdeal_sup {J K : Ideal A} (hJ : IsSubDPIdeal hI J) (hK : IsSubDPI span_IsSubDPIdeal_iff _ _ (Set.union_subset_iff.mpr ⟨hJ.1, hK.1⟩)] · intro n hn a ha rcases ha with ha | ha - . exact span_mono Set.subset_union_left (subset_span (hJ.2 n hn ha)) - . exact span_mono Set.subset_union_right (subset_span (hK.2 n hn ha)) + . exact span_mono Set.subset_union_left (subset_span (hJ.2 hn ha)) + . exact span_mono Set.subset_union_right (subset_span (hK.2 hn ha)) theorem IsSubDPIdeal_iSup {ι : Type*} {J : ι → Ideal A} (hJ : ∀ i, IsSubDPIdeal hI (J i)) : IsSubDPIdeal hI (iSup J) := by rw [iSup_eq_span, span_IsSubDPIdeal_iff _ _ (Set.iUnion_subset_iff.mpr <| fun i ↦ (hJ i).1)] simp_rw [Set.mem_iUnion] rintro n hn a ⟨i, ha⟩ - exact span_mono (Set.subset_iUnion _ i) (subset_span ((hJ i).2 n hn ha)) + exact span_mono (Set.subset_iUnion _ i) (subset_span ((hJ i).2 hn ha)) theorem IsSubDPIdeal_map_of_IsSubDPIdeal {f : A →+* B} (hf : IsDPMorphism hI hJ f) {K : Ideal A} (hK : IsSubDPIdeal hI K) : IsSubDPIdeal hJ (map f K) := by rw [Ideal.map, span_IsSubDPIdeal_iff] · rintro n hn y ⟨x, hx, rfl⟩ - exact hf.2 x (hK.1 hx) ▸ mem_map_of_mem _ (hK.2 n hn hx) + exact hf.2 x (hK.1 hx) ▸ mem_map_of_mem _ (hK.2 hn hx) · rintro y ⟨x, hx, rfl⟩ exact hf.1 (mem_map_of_mem f (hK.1 hx)) @@ -199,7 +202,7 @@ end IsSubDPIdeal structure SubDPIdeal {A : Type*} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) where carrier : Ideal A isSubideal : carrier ≤ I - dpow_mem : ∀ (n : ℕ) (_ : n ≠ 0), ∀ j ∈ carrier, hI.dpow n j ∈ carrier + dpow_mem : ∀ {n : ℕ} (_ : n ≠ 0), ∀ j ∈ carrier, hI.dpow n j ∈ carrier namespace SubDPIdeal @@ -246,21 +249,22 @@ lemma SubDPIdeal_of_IsSubDPIdeal {J : Ideal A} (hJ : IsSubDPIdeal hI J) : def prod (J : Ideal A) : SubDPIdeal hI where carrier := I • J isSubideal := mul_le_right - dpow_mem n hn x hx := by - revert n - apply @Submodule.smul_induction_on' A A _ _ _ I J _ hx - · -- mul - intro a ha b hb n hn - rw [Algebra.id.smul_eq_mul, smul_eq_mul, mul_comm a b, hI.dpow_smul ha, mul_comm] - exact Submodule.mul_mem_mul (J.pow_mem_of_mem hb n (zero_lt_iff.mpr hn)) (hI.dpow_mem hn ha) - · -- add - intro x hx y hy hx' hy' n hn - rw [hI.dpow_add' (mul_le_right hx) (mul_le_right hy)] - apply Submodule.sum_mem (I • J) - intro k _ - by_cases hk0 : k = 0 - · exact hk0 ▸ mul_mem_left (I • J) _ (hy' _ hn) - · exact mul_mem_right _ (I • J) (hx' k hk0) + dpow_mem hm x hx := by + have haux : ∀ (n : ℕ) (_ : n ≠ 0), hI.dpow n x ∈ I • J := by + apply @Submodule.smul_induction_on' A A _ _ _ I J _ hx + · -- mul + intro a ha b hb n hn + rw [Algebra.id.smul_eq_mul, smul_eq_mul, mul_comm a b, hI.dpow_smul ha, mul_comm] + exact Submodule.mul_mem_mul (J.pow_mem_of_mem hb n (zero_lt_iff.mpr hn)) (hI.dpow_mem hn ha) + · -- add + intro x hx y hy hx' hy' n hn + rw [hI.dpow_add' (mul_le_right hx) (mul_le_right hy)] + apply Submodule.sum_mem (I • J) + intro k _ + by_cases hk0 : k = 0 + · exact hk0 ▸ mul_mem_left (I • J) _ (hy' _ hn) + · exact mul_mem_right _ (I • J) (hx' k hk0) + exact @haux _ hm section CompleteLattice @@ -278,7 +282,7 @@ theorem lt_iff {J J' : SubDPIdeal hI} : J < J' ↔ J.carrier < J'.carrier := Iff instance : Top (SubDPIdeal hI) := ⟨{carrier := I isSubideal := le_refl _ - dpow_mem := fun _ hn _ hx ↦ hI.dpow_mem hn hx }⟩ + dpow_mem := fun hn _ hx ↦ hI.dpow_mem hn hx }⟩ instance inhabited : Inhabited hI.SubDPIdeal := ⟨⊤⟩ @@ -286,7 +290,7 @@ instance inhabited : Inhabited hI.SubDPIdeal := ⟨⊤⟩ instance : Bot (SubDPIdeal hI) := ⟨{carrier := ⊥ isSubideal := bot_le - dpow_mem := fun n hn x hx ↦ by rw [mem_bot.mp hx, hI.dpow_eval_zero hn, mem_bot]}⟩ + dpow_mem := fun hn x hx ↦ by rw [mem_bot.mp hx, hI.dpow_eval_zero hn, mem_bot]}⟩ --Section 1.8 of [B] -- The intersection of two sub-dp-ideals is a sub-dp-ideal. @@ -294,7 +298,7 @@ instance : Inf (SubDPIdeal hI) := ⟨fun J J' ↦ { carrier := J.carrier ⊓ J'.carrier isSubideal := fun _ hx ↦ J.isSubideal hx.1 - dpow_mem := fun n hn x hx ↦ ⟨J.dpow_mem n hn x hx.1, J'.dpow_mem n hn x hx.2⟩ }⟩ + dpow_mem := fun hn x hx ↦ ⟨J.dpow_mem hn x hx.1, J'.dpow_mem hn x hx.2⟩ }⟩ theorem inf_carrier_def (J J' : SubDPIdeal hI) : (J ⊓ J').carrier = J.carrier ⊓ J'.carrier := rfl @@ -304,9 +308,9 @@ instance : InfSet (SubDPIdeal hI) := isSubideal := fun x hx ↦ by simp only [mem_iInf] at hx exact hx ⊤ (Set.mem_insert ⊤ S) - dpow_mem := fun n hn x hx ↦ by + dpow_mem := fun hn x hx ↦ by simp only [mem_iInf] at hx ⊢ - exact fun s hs ↦ s.dpow_mem n hn x (hx s hs) }⟩ + exact fun s hs ↦ s.dpow_mem hn x (hx s hs) }⟩ theorem sInf_carrier_def (S : Set (SubDPIdeal hI)) : (sInf S).carrier = ⨅ s ∈ Insert.insert ⊤ S, (s : hI.SubDPIdeal).carrier := rfl @@ -329,7 +333,7 @@ instance : SupSet (SubDPIdeal hI) := apply subset_span apply Set.mem_biUnion hJ' obtain ⟨K, hKS, rfl⟩ := hJ' - exact K.dpow_mem n hn x h'⟩ + exact K.dpow_mem hn x h'⟩ theorem sSup_carrier_def (S : Set (SubDPIdeal hI)) : (sSup S).carrier = sSup ((toIdeal hI) '' S) := rfl @@ -383,26 +387,28 @@ def generated (S : Set A) : SubDPIdeal hI := sInf {J : SubDPIdeal hI | S ⊆ J.c def generatedDpow {S : Set A} (hS : S ⊆ I) : SubDPIdeal hI where carrier := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} isSubideal := hI.generated_dpow_isSubideal hS - dpow_mem n hn z hz := by + dpow_mem hk z hz := by have hSI := hI.generated_dpow_isSubideal hS - revert n - refine Submodule.span_induction' ?_ ?_ ?_ ?_ hz - · -- Elements of S - rintro y ⟨m, hm, x, hxS, hxy⟩ n hn - rw [hxy, hI.dpow_comp hm (hS hxS)] - exact mul_mem_left _ _ (subset_span ⟨n * m, mul_ne_zero hn hm, x, hxS, rfl⟩) - · -- Zero - exact fun _ hn ↦ by simp only [hI.dpow_eval_zero hn, zero_mem] - · intro x hx y hy hx_pow hy_pow n hn - rw [hI.dpow_add' (hSI hx) (hSI hy)] - apply Submodule.sum_mem (span _) - intro m _ - by_cases hm0 : m = 0 - · rw [hm0]; exact (span _).mul_mem_left _ (hy_pow n hn) - · exact (span _).mul_mem_right _ (hx_pow m hm0) - · intro a x hx hx_pow n hn - rw [smul_eq_mul, hI.dpow_smul (hSI hx)] - exact mul_mem_left (span _) (a ^ n) (hx_pow n hn) + have haux : ∀ (n : ℕ) (_ : n ≠ 0), + hI.dpow n z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} := by + refine Submodule.span_induction' ?_ ?_ ?_ ?_ hz + · -- Elements of S + rintro y ⟨m, hm, x, hxS, hxy⟩ n hn + rw [hxy, hI.dpow_comp hm (hS hxS)] + exact mul_mem_left _ _ (subset_span ⟨n * m, mul_ne_zero hn hm, x, hxS, rfl⟩) + · -- Zero + exact fun _ hn ↦ by simp only [hI.dpow_eval_zero hn, zero_mem] + · intro x hx y hy hx_pow hy_pow n hn + rw [hI.dpow_add' (hSI hx) (hSI hy)] + apply Submodule.sum_mem (span _) + intro m _ + by_cases hm0 : m = 0 + · rw [hm0]; exact (span _).mul_mem_left _ (hy_pow n hn) + · exact (span _).mul_mem_right _ (hx_pow m hm0) + · intro a x hx hx_pow n hn + rw [smul_eq_mul, hI.dpow_smul (hSI hx)] + exact mul_mem_left (span _) (a ^ n) (hx_pow n hn) + exact haux _ hk theorem generatedDpow_carrier {S : Set A} (hS : S ⊆ I) : (generatedDpow hI hS).carrier = @@ -415,7 +421,7 @@ theorem generated_dpow_le (S : Set A) (J : SubDPIdeal hI) (hSJ : S ⊆ J.carrier span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ J.carrier := by rw [span_le] rintro y ⟨n, hn, x, hx, hxy⟩ - exact hxy ▸ J.dpow_mem n hn x (hSJ hx) + exact hxy ▸ J.dpow_mem hn x (hSJ hx) theorem generated_carrier_eq {S : Set A} (hS : S ⊆ I) : (generated hI S).carrier = @@ -457,7 +463,7 @@ open Ideal def DPMorphism.ker (f : DPMorphism hI hJ) : SubDPIdeal hI where carrier := RingHom.ker f.toRingHom ⊓ I isSubideal := inf_le_right - dpow_mem n hn a := by + dpow_mem hn a := by simp only [mem_inf, and_imp, RingHom.mem_ker] intro ha ha' rw [← f.isDPMorphism.2 a ha', ha] @@ -496,12 +502,12 @@ theorem mem_dpEqualizer_iff {A : Type*} [CommSemiring A] {I : Ideal A} (hI hI' : theorem dpEqualizer_is_dp_ideal_left {A : Type*} [CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) : DividedPowers.IsSubDPIdeal hI (dpEqualizer hI hI') := - IsSubDPIdeal.mk (fun _ hx ↦ hx.1) (fun n hn x hx ↦ ⟨hI.dpow_mem hn hx.1, + IsSubDPIdeal.mk (fun _ hx ↦ hx.1) (fun hn x hx ↦ ⟨hI.dpow_mem hn hx.1, fun m ↦ by rw [hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]⟩) theorem dpEqualizer_is_dp_ideal_right {A : Type*} [CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) : DividedPowers.IsSubDPIdeal hI' (dpEqualizer hI hI') := - IsSubDPIdeal.mk (fun _ hx ↦ hx.1) (fun n hn x hx ↦ ⟨hI'.dpow_mem hn hx.1, fun m ↦ by + IsSubDPIdeal.mk (fun _ hx ↦ hx.1) (fun hn x hx ↦ ⟨hI'.dpow_mem hn hx.1, fun m ↦ by rw [← hx.2, hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]⟩) open Ideal @@ -520,9 +526,9 @@ def interQuot {A : Type*} [CommRing A] {I : Ideal A} (hI : DividedPowers I) (J : Ideal A) (hJ : DividedPowers (I.map (Ideal.Quotient.mk J))) (φ : DPMorphism hI hJ) (hφ : φ.toRingHom = Ideal.Quotient.mk J) : SubDPIdeal hI where - carrier := J ⊓ I + carrier := J ⊓ I isSubideal := by simp only [ge_iff_le, inf_le_right] - dpow_mem := fun n hn a ⟨haJ, haI⟩ ↦ by + dpow_mem := fun hn a ⟨haJ, haI⟩ ↦ by refine ⟨?_, hI.dpow_mem hn haI⟩ rw [SetLike.mem_coe, ← Quotient.eq_zero_iff_mem, ← hφ, ← φ.dpow_comp a haI] suffices ha0 : φ.toRingHom a = 0 by