Skip to content

Commit

Permalink
chore(RingTheory/DividedPowers/Basic): make variables implicit (#22166)
Browse files Browse the repository at this point in the history 
Co-authored-by: AntoineChambert-Loir <[email protected]>
  • Loading branch information
@mariainesdff @AntoineChambert-Loir
mariainesdff and AntoineChambert-Loir committed Feb 26, 2025
1 parent f598df3 commit d41e468
Showing 1 changed file with 47 additions and 56 deletions.
103 changes: 47 additions & 56 deletions Mathlib/RingTheory/DividedPowers/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@ collected by the structure `DividedPowers`. The list of axioms is embedded in th
To avoid coercions, we rather consider `DividedPowers.dpow : ℕ → A → A`, extended by 0.
* `DividedPowers.dpow_null` asserts that `dpow n x = 0` for `x ∉ I`
* `DividedPowers.dpow_mem` : `dpow n x ∈ I` for `n ≠ 0`
For `x y : A` and `m n : ℕ` such that `x ∈ I` and `y ∈ I`, one has
* `DividedPowers.dpow_zero` : `dpow 0 x = 1`
Expand All @@ -28,22 +27,15 @@ this is the binomial theorem without binomial coefficients.
* `DividedPowers.dpow_mul`: `dpow n (a * x) = a ^ n * dpow n x`
* `DividedPowers.mul_dpow` : `dpow m x * dpow n x = choose (m + n) m * dpow (m + n) x`
* `DividedPowers.dpow_comp` : `dpow m (dpow n x) = uniformBell m n * dpow (m * n) x`
* `DividedPowers.dividedPowersBot` : the trivial divided powers structure on the zero ideal
* `DividedPowers.prod_dpow`: a product of divided powers is a multinomial coefficients
times a divided power
* `DividedPowers.dpow_sum`: the multinomial theorem for divided powers,
without multinomial coefficients.
* `DividedPowers.ofRingEquiv`: transfer divided powers along `RingEquiv`
* `DividedPowers.equiv`: the equivalence `DividedPowers I ≃ DividedPowers J`,
for `e : R ≃+* S`, and `I : Ideal R`, `J : Ideal S` such that `I.map e = J`
* `DividedPowers.exp`: the power series `Σ (dpow n a) X ^n`
* `DividedPowers.exp_add`: its multiplicativity
## References
Expand Down Expand Up @@ -85,13 +77,13 @@ structure DividedPowers where
dpow_zero : ∀ {x} (_ : x ∈ I), dpow 0 x = 1
dpow_one : ∀ {x} (_ : x ∈ I), dpow 1 x = x
dpow_mem : ∀ {n x} (_ : n ≠ 0) (_ : x ∈ I), dpow n x ∈ I
dpow_add : ∀ (n) {x y} (_ : x ∈ I) (_ : y ∈ I),
dpow_add : ∀ {n} {x y} (_ : x ∈ I) (_ : y ∈ I),
dpow n (x + y) = (antidiagonal n).sum fun k ↦ dpow k.1 x * dpow k.2 y
dpow_mul : ∀ (n) {a : A} {x} (_ : x ∈ I),
dpow_mul : ∀ {n} {a : A} {x} (_ : x ∈ I),
dpow n (a * x) = a ^ n * dpow n x
mul_dpow : ∀ (m n) {x} (_ : x ∈ I),
mul_dpow : ∀ {m n} {x} (_ : x ∈ I),
dpow m x * dpow n x = choose (m + n) m * dpow (m + n) x
dpow_comp : ∀ (m) {n x} (_ : n ≠ 0) (_ : x ∈ I),
dpow_comp : ∀ {m n x} (_ : n ≠ 0) (_ : x ∈ I),
dpow m (dpow n x) = uniformBell m n * dpow (m * n) x

variable (A) in
Expand All @@ -103,15 +95,15 @@ def dividedPowersBot [DecidableEq A] : DividedPowers (⊥ : Ideal A) where
dsimp
rw [if_neg]
exact not_and_of_not_left (n = 0) ha
dpow_zero {a} ha := by
dpow_zero ha := by
rw [mem_bot.mp ha]
simp only [and_self, ite_true]
dpow_one {a} ha := by
dpow_one ha := by
simp [mem_bot.mp ha]
dpow_mem {n a} hn _ := by
simp only [mem_bot, ite_eq_right_iff, and_imp]
exact fun _ a ↦ False.elim (hn a)
dpow_add n a b ha hb := by
dpow_add ha hb := by
rw [mem_bot.mp ha, mem_bot.mp hb, add_zero]
simp only [true_and, ge_iff_le, tsub_eq_zero_iff_le, mul_ite, mul_one, mul_zero]
split_ifs with h
Expand All @@ -126,13 +118,13 @@ def dividedPowersBot [DecidableEq A] : DividedPowers (⊥ : Ideal A) where
exact h hi.symm
· rfl
· rfl
dpow_mul n {a x} hx := by
dpow_mul {n} _ _ hx := by
rw [mem_bot.mp hx]
simp only [mul_zero, true_and, mul_ite, mul_one]
by_cases hn : n = 0
· rw [if_pos hn, hn, if_pos rfl, _root_.pow_zero]
· simp only [if_neg hn]
mul_dpow m n {x} hx := by
mul_dpow {m n x} hx := by
rw [mem_bot.mp hx]
simp only [true_and, mul_ite, mul_one, mul_zero, add_eq_zero]
by_cases hn : n = 0
Expand Down Expand Up @@ -183,9 +175,9 @@ section BasicLemmas
variable {A : Type*} [CommSemiring A] {I : Ideal A} {a b : A}

/-- Variant of `DividedPowers.dpow_add` with a sum on `range (n + 1)` -/
theorem dpow_add' (hI : DividedPowers I) (n : ℕ) (ha : a ∈ I) (hb : b ∈ I) :
theorem dpow_add' (hI : DividedPowers I) {n : ℕ} (ha : a ∈ I) (hb : b ∈ I) :
hI.dpow n (a + b) = (range (n + 1)).sum fun k ↦ hI.dpow k a * hI.dpow (n - k) b := by
rw [hI.dpow_add n ha hb, sum_antidiagonal_eq_sum_range_succ_mk]
rw [hI.dpow_add ha hb, sum_antidiagonal_eq_sum_range_succ_mk]

/-- The exponential series of an element in the context of divided powers,
`Σ (dpow n a) X ^ n` -/
Expand All @@ -203,36 +195,36 @@ theorem exp_add' (dp : ℕ → A → A)

theorem exp_add (hI : DividedPowers I) (ha : a ∈ I) (hb : b ∈ I) :
hI.exp (a + b) = hI.exp a * hI.exp b :=
exp_add' _ (fun n ↦ hI.dpow_add n ha hb)
exp_add' _ (fun _ ↦ hI.dpow_add ha hb)

variable (hI : DividedPowers I)

/- ## Rewriting lemmas -/

theorem dpow_smul (n : ℕ) (ha : a ∈ I) :
theorem dpow_smul {n : ℕ} (ha : a ∈ I) :
hI.dpow n (b • a) = b ^ n • hI.dpow n a := by
simp only [smul_eq_mul, hI.dpow_mul, ha]

theorem dpow_mul_right (n : ℕ) (ha : a ∈ I) :
theorem dpow_mul_right {n : ℕ} (ha : a ∈ I) :
hI.dpow n (a * b) = hI.dpow n a * b ^ n := by
rw [mul_comm, hI.dpow_mul n ha, mul_comm]
rw [mul_comm, hI.dpow_mul ha, mul_comm]

theorem dpow_smul_right (n : ℕ) (ha : a ∈ I) :
theorem dpow_smul_right {n : ℕ} (ha : a ∈ I) :
hI.dpow n (a • b) = hI.dpow n a • b ^ n := by
rw [smul_eq_mul, hI.dpow_mul_right n ha, smul_eq_mul]
rw [smul_eq_mul, hI.dpow_mul_right ha, smul_eq_mul]

theorem factorial_mul_dpow_eq_pow (n : ℕ) (ha : a ∈ I) :
theorem factorial_mul_dpow_eq_pow {n : ℕ} (ha : a ∈ I) :
(n ! : A) * hI.dpow n a = a ^ n := by
induction n with
| zero => rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
| succ n ih =>
rw [factorial_succ, mul_comm (n + 1)]
nth_rewrite 1 [← (n + 1).choose_one_right]
rw [← choose_symm_add, cast_mul, mul_assoc,
← hI.mul_dpow n 1 ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]

theorem dpow_eval_zero {n : ℕ} (hn : n ≠ 0) : hI.dpow n 0 = 0 := by
rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_mul n I.zero_mem,
rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_mul I.zero_mem,
zero_pow hn, zero_mul, zero_mul]

/-- If an element of a divided power ideal is killed by multiplication
Expand All @@ -244,7 +236,7 @@ theorem nilpotent_of_mem_dpIdeal {n : ℕ} (hn : n ≠ 0) (hnI : ∀ {y} (_ : y
have h_fac : (n ! : A) * hI.dpow n a =
n • ((n - 1)! : A) * hI.dpow n a := by
rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred (Nat.pos_of_ne_zero hn)]
rw [← hI.factorial_mul_dpow_eq_pow n ha, h_fac, smul_mul_assoc]
rw [← hI.factorial_mul_dpow_eq_pow ha, h_fac, smul_mul_assoc]
exact hnI (I.mul_mem_left ((n - 1)! : A) (hI.dpow_mem hn ha))

/-- If J is another ideal of A with divided powers,
Expand All @@ -255,20 +247,20 @@ theorem coincide_on_smul {J : Ideal A} (hJ : DividedPowers J) {n : ℕ} (ha : a
hI.dpow n a = hJ.dpow n a := by
induction ha using Submodule.smul_induction_on' generalizing n with
| smul a ha b hb =>
rw [Algebra.id.smul_eq_mul, hJ.dpow_mul n hb, mul_comm a b, hI.dpow_mul n ha, ←
hJ.factorial_mul_dpow_eq_pow n hb, ← hI.factorial_mul_dpow_eq_pow n ha]
rw [Algebra.id.smul_eq_mul, hJ.dpow_mul hb, mul_comm a b, hI.dpow_mul ha,
← hJ.factorial_mul_dpow_eq_pow hb, ← hI.factorial_mul_dpow_eq_pow ha]
ring
| add x hx y hy hx' hy' =>
rw [hI.dpow_add n (mul_le_right hx) (mul_le_right hy),
hJ.dpow_add n (mul_le_left hx) (mul_le_left hy)]
rw [hI.dpow_add (mul_le_right hx) (mul_le_right hy),
hJ.dpow_add (mul_le_left hx) (mul_le_left hy)]
apply sum_congr rfl
intro k _
rw [hx', hy']

/-- A product of divided powers is a multinomial coefficient times the divided power
[Roby-1965], formula (III') -/
theorem prod_dpow {ι : Type*} {s : Finset ι} (n : ι → ℕ) (ha : a ∈ I) :
theorem prod_dpow {ι : Type*} {s : Finset ι} {n : ι → ℕ} (ha : a ∈ I) :
(s.prod fun i ↦ hI.dpow (n i) a) = multinomial s n * hI.dpow (s.sum n) a := by
classical
induction s using Finset.induction with
Expand All @@ -277,7 +269,7 @@ theorem prod_dpow {ι : Type*} {s : Finset ι} (n : ι → ℕ) (ha : a ∈ I) :
rw [hI.dpow_zero ha]
| insert hi hrec =>
rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
mul_assoc, mul_dpow _ _ _ ha, ← sum_insert hi, ← mul_assoc]
mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]
apply congr_arg₂ _ _ rfl
rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

Expand All @@ -286,10 +278,10 @@ theorem prod_dpow {ι : Type*} {s : Finset ι} (n : ι → ℕ) (ha : a ∈ I) :
/-- Lemma towards `dpow_sum` when we only have partial information on a divided power ideal -/
theorem dpow_sum' {M : Type*} [AddCommMonoid M] {I : AddSubmonoid M} (dpow : ℕ → M → A)
(dpow_zero : ∀ {x} (_ : x ∈ I), dpow 0 x = 1)
(dpow_add : ∀ (n) {x y} (_ : x ∈ I) (_ : y ∈ I),
(dpow_add : ∀ {n x y} (_ : x ∈ I) (_ : y ∈ I),
dpow n (x + y) = (antidiagonal n).sum fun k ↦ dpow k.1 x * dpow k.2 y)
(dpow_eval_zero : ∀ {n : ℕ} (_ : n ≠ 0), dpow n 0 = 0)
{ι : Type*} [DecidableEq ι] {s : Finset ι} {x : ι → M} (hx : ∀ i ∈ s, x i ∈ I) (n : ℕ) :
{ι : Type*} [DecidableEq ι] {s : Finset ι} {x : ι → M} (hx : ∀ i ∈ s, x i ∈ I) {n : ℕ} :
dpow n (s.sum x) = (s.sym n).sum fun k ↦ s.prod fun i ↦ dpow (Multiset.count i k) (x i) := by
simp only [sum_antidiagonal_eq_sum_range_succ_mk] at dpow_add
induction s using Finset.induction generalizing n with
Expand All @@ -307,7 +299,7 @@ theorem dpow_sum' {M : Type*} [AddCommMonoid M] {I : AddSubmonoid M} (dpow : ℕ
-- This should be golfable using `Finset.symInsertEquiv`
have hx' : ∀ i, i ∈ s → x i ∈ I := fun i hi ↦ hx i (mem_insert_of_mem hi)
simp_rw [sum_insert ha,
dpow_add n (hx a (mem_insert_self a s)) (I.sum_mem fun i ↦ hx' i),
dpow_add (hx a (mem_insert_self a s)) (I.sum_mem fun i ↦ hx' i),
sum_range, ih hx', mul_sum, sum_sigma', eq_comm]
apply sum_bij'
(fun m _ ↦ m.filterNe a)
Expand Down Expand Up @@ -337,10 +329,10 @@ theorem dpow_sum' {M : Type*} [AddCommMonoid M] {I : AddSubmonoid M} (dpow : ℕ

/-- A “multinomial” theorem for divided powers — without multinomial coefficients -/
theorem dpow_sum {ι : Type*} [DecidableEq ι] {s : Finset ι} {x : ι → A}
(hx : ∀ i ∈ s, x i ∈ I) (n : ℕ) :
(hx : ∀ i ∈ s, x i ∈ I) {n : ℕ} :
hI.dpow n (s.sum x) =
(s.sym n).sum fun k ↦ s.prod fun i ↦ hI.dpow (Multiset.count i k) (x i) :=
dpow_sum' hI.dpow hI.dpow_zero hI.dpow_add hI.dpow_eval_zero hx n
dpow_sum' hI.dpow hI.dpow_zero hI.dpow_add hI.dpow_eval_zero hx

end BasicLemmas

Expand All @@ -353,47 +345,47 @@ variable {A B : Type*} [CommSemiring A] {I : Ideal A} [CommSemiring B] {J : Idea
/-- Transfer divided powers under an equivalence -/
def ofRingEquiv (hI : DividedPowers I) : DividedPowers J where
dpow n b := e (hI.dpow n (e.symm b))
dpow_null {n} {x} hx := by
dpow_null hx := by
rw [EmbeddingLike.map_eq_zero_iff, hI.dpow_null]
rwa [symm_apply_mem_of_equiv_iff, h]
dpow_zero {x} hx := by
dpow_zero hx := by
rw [EmbeddingLike.map_eq_one_iff, hI.dpow_zero]
rwa [symm_apply_mem_of_equiv_iff, h]
dpow_one {x} hx := by
dpow_one hx := by
simp only
rw [dpow_one, RingEquiv.apply_symm_apply]
rwa [I.symm_apply_mem_of_equiv_iff, h]
dpow_mem {n} {x} hn hx := by
dpow_mem hn hx := by
simp only
rw [← h, I.apply_mem_of_equiv_iff]
apply hI.dpow_mem hn
rwa [I.symm_apply_mem_of_equiv_iff, h]
dpow_add n {x y} hx hy := by
dpow_add hx hy := by
simp only [map_add]
rw [hI.dpow_add n (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))
rw [hI.dpow_add (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))
(symm_apply_mem_of_equiv_iff.mpr (h ▸ hy))]
simp only [map_sum, _root_.map_mul]
dpow_mul n {a x} hx := by
dpow_mul hx := by
simp only [_root_.map_mul]
rw [hI.dpow_mul n (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))]
rw [hI.dpow_mul (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))]
rw [_root_.map_mul, map_pow]
simp only [RingEquiv.apply_symm_apply]
mul_dpow m n {x} hx := by
mul_dpow hx := by
simp only
rw [← _root_.map_mul, hI.mul_dpow, _root_.map_mul]
· simp only [map_natCast]
· rwa [symm_apply_mem_of_equiv_iff, h]
dpow_comp m {n x} hn hx := by
dpow_comp hn hx := by
simp only [RingEquiv.symm_apply_apply]
rw [hI.dpow_comp _ hn]
rw [hI.dpow_comp hn]
· simp only [_root_.map_mul, map_natCast]
· rwa [symm_apply_mem_of_equiv_iff, h]

@[simp]
theorem ofRingEquiv_dpow (hI : DividedPowers I) (n : ℕ) (b : B) :
theorem ofRingEquiv_dpow (hI : DividedPowers I) {n : ℕ} {b : B} :
(ofRingEquiv h hI).dpow n b = e (hI.dpow n (e.symm b)) := rfl

theorem ofRingEquiv_dpow_apply (hI : DividedPowers I) (n : ℕ) (a : A) :
theorem ofRingEquiv_dpow_apply (hI : DividedPowers I) {n : ℕ} {a : A} :
(ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a) := by
simp

Expand All @@ -408,11 +400,10 @@ theorem equiv_apply (hI : DividedPowers I) (n : ℕ) (b : B) :
(equiv h hI).dpow n b = e (hI.dpow n (e.symm b)) := rfl

/-- Variant of `DividedPowers.equiv_apply` -/
theorem equiv_apply' (hI : DividedPowers I) (n : ℕ) (a : A) :
theorem equiv_apply' (hI : DividedPowers I) {n : ℕ} {a : A} :
(equiv h hI).dpow n (e a) = e (hI.dpow n a) :=
ofRingEquiv_dpow_apply h hI n a
ofRingEquiv_dpow_apply h hI

end Equiv

end DividedPowers

0 comments on commit d41e468

Please sign in to comment.