feat(RingTheory/DividedPowerAlgebra/Init): add universal divided power algebra (leanprover-community#35804)

We define the universal divided power algebra of an `R`-module `M`.

Co-authored by @AntoineChambert-Loir

Co-authored-by: mariainesdff <mariaines.dff@gmail.com>

Author: mariainesdff

Mathlib.lean

@@ -6252,6 +6252,7 @@ public import Mathlib.RingTheory.Derivation.ToSquareZero
 public import Mathlib.RingTheory.DiscreteValuationRing.Basic
 public import Mathlib.RingTheory.DiscreteValuationRing.TFAE
 public import Mathlib.RingTheory.Discriminant
+public import Mathlib.RingTheory.DividedPowerAlgebra.Init
 public import Mathlib.RingTheory.DividedPowers.Basic
 public import Mathlib.RingTheory.DividedPowers.DPMorphism
 public import Mathlib.RingTheory.DividedPowers.Padic

Mathlib/RingTheory/DividedPowerAlgebra/Init.lean

@@ -0,0 +1,265 @@
+/-
+Copyright (c) 2026 Antoine Chambert-Loir & María Inés de Frutos—Fernández. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Chambert-Loir, María Inés de Frutos—Fernández
+-/
+module
+
+public import Mathlib.Algebra.RingQuot
+public import Mathlib.RingTheory.DividedPowers.Basic
+
+/-!
+# The universal divided power algebra
+
+Let `R` be a ring and `M` be an `R`-module. In this file we define `Γ_R(M)`, the universal
+divided power algebra of `M`, as the ring quotient of the polynomial ring in the variables `ℕ × M`
+by the relation `DividedPowerAlgebra.Rel`.
+
+`DividedPowerAlgebra R M` satisfies a weak universal property for morphisms to rings with
+divided_powers.
+
+## Main definitions
+
+* `DividedPowerAlgebra.Rel`: the type coding the basic relations that will give rise to the
+  divided power algebra. The class of `X (n, a)` will be equal to `dpow n a`, for `a ∈ M`.
+
+* `DividedPowerAlgebra R M`: the universal divided power algebra of the `R`-module `M`.
+
+* `DividedPowerAlgebra.dp R n m`: the equivalence class of `X (⟨n, m⟩)` in
+  `DividedPowerAlgebra R M`.
+
+## TODO
+
+* Add the weak universal property of `DividedPowerAlgebra R M`.
+* Show in upcoming files that `DividedPowerAlgebra R M` has divided powers.
+
+-/
+
+@[expose] public section
+noncomputable section
+
+open Finset Ideal MvPolynomial RingQuot
+
+variable (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M]
+
+namespace DividedPowerAlgebra
+
+/-- The type coding the basic relations that will give rise to the divided power algebra.
+  The class of `X (n, a)` will be equal to `dpow n a`, for `a ∈ M`. -/
+inductive Rel : (MvPolynomial (ℕ × M) R) → (MvPolynomial (ℕ × M) R) → Prop
+  | rfl_zero : Rel 0 0 -- Needed for technical reasons.
+  | zero {a : M} : Rel (X (0, a)) 1
+  | smul {r : R} {n : ℕ} {a : M} : Rel (X (n, r • a)) (r ^ n • X (n, a))
+  | mul {m n : ℕ} {a : M} : Rel (X (m, a) * X (n, a)) (Nat.choose (m + n) m • X (m + n, a))
+  | add {n : ℕ} {a b : M} :
+    Rel (X (n, a + b)) ((Finset.antidiagonal n).sum fun k => X (k.1, a) * X (k.2, b))
+
+/-- The ideal of `MvPolynomial (ℕ × M) R` generated by `Rel`. -/
+def RelI : Ideal (MvPolynomial (ℕ × M) R) := ofRel (DividedPowerAlgebra.Rel R M)
+
+end DividedPowerAlgebra
+
+/-- The divided power algebra of a module M is defined as the ring quotient of the polynomial ring
+  in the variables `ℕ × M` by the ring relation defined by `DividedPowerAlgebra.Rel`.
+  We will later show that that `DividedPowerAlgebra R M` has divided powers.
+  It satisfies a weak universal property for morphisms to rings with divided_powers. -/
+abbrev DividedPowerAlgebra := RingQuot (DividedPowerAlgebra.Rel R M)
+
+namespace DividedPowerAlgebra
+
+open MvPolynomial
+
+variable {R M}
+
+lemma mkAlgHom_surjective : Function.Surjective (mkAlgHom R (Rel R M)) :=
+  RingQuot.mkAlgHom_surjective _ _
+
+lemma mkAlgHom_C (a : R) :
+    mkAlgHom R (Rel R M) (C a) = algebraMap R (DividedPowerAlgebra R M) a := by
+  rw [← MvPolynomial.algebraMap_eq, AlgHom.commutes]
+
+lemma mkRingHom_C (a : R) :
+    mkRingHom (Rel R M) (C a) = algebraMap R (DividedPowerAlgebra R M) a := by
+  rw [← mkAlgHom_C, mkAlgHom, AlgHom.coe_mk]
+
+variable (R)
+
+/-- `dp R n m` is the equivalence class of `X (⟨n, m⟩)` in `DividedPowerAlgebra R M`. -/
+def dp (n : ℕ) (m : M) : DividedPowerAlgebra R M := mkAlgHom R (Rel R M) (X ⟨n, m⟩)
+
+theorem dp_def (n : ℕ) (m : M) :
+  dp R n m = mkAlgHom R (Rel R M) (X ⟨n, m⟩) := rfl
+
+protected theorem induction_on' {P : DividedPowerAlgebra R M → Prop} (f : DividedPowerAlgebra R M)
+    (h_C : ∀ a, P (mkAlgHom R (Rel R M) (C a))) (h_add : ∀ f g, P f → P g → P (f + g))
+    (h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)) : P f := by
+  obtain ⟨F, hf⟩ := RingQuot.mkRingHom_surjective (DividedPowerAlgebra.Rel R M) f
+  rw [← hf]
+  induction F using MvPolynomial.induction_on generalizing f with
+  | C a =>
+      convert h_C a using 1
+      rw [mkAlgHom, AlgHom.coe_mk]
+  | add g1 g2 hg1 hg2 =>
+      rw [map_add]
+      exact h_add _ _ (hg1 ((mkRingHom (Rel R M)) g1) rfl) (hg2 ((mkRingHom (Rel R M)) g2) rfl)
+  | mul_X g nm h =>
+      have h' : (mkRingHom (Rel R M)) (X nm) = dp R nm.1 nm.2 := by
+        simp only [dp_def, Prod.mk.eta, mkAlgHom, AlgHom.coe_mk]
+      rw [_root_.map_mul, h']
+      exact h_dp _ _ _ (h (mkRingHom (Rel R M) g) rfl)
+
+@[elab_as_elim]
+protected theorem induction_on {P : DividedPowerAlgebra R M → Prop} (f : DividedPowerAlgebra R M)
+    (h_C : ∀ a, P (algebraMap R _ a)) (h_add : ∀ f g, P f → P g → P (f + g))
+    (h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)) : P f :=
+  DividedPowerAlgebra.induction_on' R f (fun a => by rw [mkAlgHom_C]; exact h_C a) h_add h_dp
+
+theorem dp_eq_mkRingHom (n : ℕ) (m : M) :
+    dp R n m = mkRingHom (Rel R M) (X (⟨n, m⟩)) := by
+  simp [dp, mkRingHom, mkAlgHom]
+
+theorem dp_zero (m : M) : dp R 0 m = 1 := by
+  rw [dp_def, ← map_one (mkAlgHom R (Rel R M))]
+  exact RingQuot.mkAlgHom_rel R Rel.zero
+
+theorem dp_smul (r : R) (n : ℕ) (m : M) : dp R n (r • m) = r ^ n • dp R n m := by
+  rw [dp_def, dp_def, ← map_smul]
+  exact mkAlgHom_rel R Rel.smul
+
+theorem dp_null (n : ℕ) : dp R n (0 : M) = if n = 0 then 1 else 0 := by
+  cases Nat.eq_zero_or_pos n with
+  | inl hn =>
+    rw [if_pos hn, hn, dp_zero]
+  | inr hn =>
+    rw [if_neg (ne_of_gt hn), ← zero_smul R (0 : M), dp_smul]
+    rw [zero_pow (Nat.pos_iff_ne_zero.mp hn), zero_smul]
+
+theorem dp_null_of_ne_zero {n : ℕ} (hn : n ≠ 0) : dp R n (0 : M) = 0 := by
+  rw [dp_null R n, if_neg hn]
+
+theorem dp_mul (n p : ℕ) (m : M) :
+    dp R n m * dp R p m = (n + p).choose n • dp R (n + p) m := by
+  simp only [dp_def, ← _root_.map_mul, ← map_nsmul]
+  exact mkAlgHom_rel R Rel.mul
+
+theorem dp_add (n : ℕ) (x y : M) :
+    dp R n (x + y) = (antidiagonal n).sum fun k => dp R k.1 x * dp R k.2 y := by
+  simp only [dp_def]
+  rw [mkAlgHom_rel (A := MvPolynomial (ℕ × M) R) R Rel.add, map_sum,
+    Finset.sum_congr rfl (fun k _ ↦ by rw [_root_.map_mul])]
+
+theorem dp_sum {ι : Type*} [DecidableEq ι] (s : Finset ι) (q : ℕ) (x : ι → M) :
+    dp R q (s.sum x) =
+      (Finset.sym s q).sum fun k => s.prod fun i => dp R (Multiset.count i k) (x i) :=
+  DividedPowers.dpow_sum' (I := ⊤) _ (fun {m} _ ↦ dp_zero R m)
+    (fun {n x y} _ _ ↦ dp_add R n x y) (dp_null_of_ne_zero R) (fun _ _ ↦ trivial)
+
+theorem dp_sum_smul {ι : Type*} [DecidableEq ι] (s : Finset ι) (q : ℕ) (a : ι → R) (x : ι → M) :
+    dp R q (s.sum fun i => a i • x i) =
+      (Finset.sym s q).sum fun k =>
+        (s.prod fun i => a i ^ Multiset.count i k) •
+          s.prod fun i => dp R (Multiset.count i k) (x i) := by
+  simp_rw [dp_sum, dp_smul, Algebra.smul_def, map_prod, ← Finset.prod_mul_distrib]
+
+open Nat in
+lemma prod_dp {ι : Type*} (s : Finset ι) {n : ι → ℕ} (m : M) :
+    ∏ i ∈ s, (dp R (n i) m) = (Nat.multinomial s n) * dp R (s.sum n) m := by
+  classical
+  induction s using Finset.induction with
+  | empty =>
+    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul, dp_zero]
+  | insert _ _ hi hrec =>
+    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (dp R (n _) m),
+      mul_assoc, dp_mul, ← sum_insert hi, nsmul_eq_mul, ← mul_assoc]
+    congr 1
+    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
+
+open scoped Nat
+
+theorem natFactorial_mul_dp_eq (n : ℕ) (x : M) :
+    n ! * dp R n x = (dp R 1 x) ^ n := by
+  induction n with
+  | zero => simp [dp_zero]
+  | succ n h =>
+    rw [pow_succ, ← h, mul_assoc, dp_mul, nsmul_eq_mul, ← mul_assoc, ← Nat.cast_mul]
+    simp [mul_comm _ (n + 1), Nat.factorial_succ]
+
+variable (M) in
+/-- The canonical linear map `M →ₗ[R] DividedPowerAlgebra R M`. -/
+def embed : M →ₗ[R] DividedPowerAlgebra R M where
+  toFun m   := dp R 1 m
+  map_add' _ _  := by simp [dp_add, Nat.antidiagonal_succ, dp_zero, add_comm]
+  map_smul' _ _ := by simp [dp_smul, pow_one, RingHom.id_apply]
+
+theorem embed_def (m : M) : embed R M m = dp R 1 m := rfl
+
+variable {R}
+
+theorem algHom_ext_iff {A : Type*} [CommSemiring A] [Algebra R A]
+    {f g : DividedPowerAlgebra R M →ₐ[R] A} :
+    (f = g) ↔ (∀ n m, f (dp R n m) = g (dp R n m)) := by
+  refine ⟨fun h _ _ ↦ by rw [h], fun h ↦ ?_⟩
+  rw [DFunLike.ext'_iff]
+  apply Function.Surjective.injective_comp_right mkAlgHom_surjective
+  simpa [← AlgHom.coe_comp] using MvPolynomial.algHom_ext fun ⟨n, m⟩ => h n m
+
+@[ext]
+theorem algHom_ext {A : Type*} [CommSemiring A] [Algebra R A]
+    {f g : DividedPowerAlgebra R M →ₐ[R] A}
+    (h : ∀ n m, f (dp R n m) = g (dp R n m)) : f = g :=
+  algHom_ext_iff.mpr h
+
+section
+
+open Submodule
+
+variable {R M ι : Type*} [CommRing R] [AddCommGroup M] [Module R M] {v : ι → M}
+
+/- If the `R`-module is spanned by elements `v i`, then `DividedPowerAlgebra R M`
+is linearly spanned by the finite products `∏ i, dp R (k i) (v i)`.
+
+When these `v i` form a `Module.Basis`, these elements are linearly independent,
+hence form a `Module.Basis` of `DividedPowerAlgebra R M`, see `DividedPowers.DPAlgebra.Free`. -/
+theorem submodule_span_prod_dp_eq_top (hv : span R (Set.range v) = ⊤) :
+    span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun i k ↦ dp R k (v i)) = ⊤ := by
+  rw [eq_top_iff]
+  intro p hp
+  clear hp
+  induction p using DividedPowerAlgebra.induction_on with
+  | h_C r =>
+    simp only [Algebra.algebraMap_eq_smul_one]
+    exact smul_mem _ _ (subset_span ⟨0, by simp⟩)
+  | h_add x y hx hy => exact Submodule.add_mem _ hx hy
+  | h_dp x k m hx =>
+    have hm : m ∈ span R (Set.range v) := by simp [hv, mem_top]
+    induction hm using span_induction generalizing x k with
+    | zero => rw [dp_null]; split_ifs <;> simp [hx]
+    | smul r m hm h => simp [dp_smul, smul_mem _ _ (h x k hx)]
+    | mem y hy =>
+      obtain ⟨i, rfl⟩ := hy
+      induction hx using span_induction with
+      | zero => simp
+      | mem x hx =>
+        obtain ⟨n, rfl⟩ := hx
+        simp only
+        rw [← n.mul_prod_erase' i _ (fun i ↦ dp_zero R (v i)), mul_comm,
+          ← mul_assoc, dp_mul, nsmul_eq_mul, mul_assoc, ← nsmul_eq_mul]
+        refine smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)
+        simp only
+        rw [← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero _ (v i))]
+        simp
+      | add x y hxmem hymem hx hy =>
+        rw [add_mul]
+        exact Submodule.add_mem _ hx hy
+      | smul r x hxmem hx =>
+        rw [smul_mul_assoc]
+        exact smul_mem _ _ hx
+    | add m n hm_mem hn_mem hm hn =>
+      rw [dp_add, mul_sum]
+      apply sum_mem (fun c hc ↦ ?_)
+      rw [← mul_assoc]
+      exact hn (x * dp R c.1 m) c.2 (hm x c.1 hx)
+
+end
+
+end DividedPowerAlgebra