feat(RingTheory.DividedPowerAlgebra.Init.lean): add weak universal property and functoriality (leanprover-community#36434)

Co-authored by @AntoineChambert-Loir.

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

Author: mariainesdff

Mathlib/RingTheory/DividedPowerAlgebra/Init.lean

@@ -5,6 +5,7 @@ Authors: Antoine Chambert-Loir, María Inés de Frutos—Fernández
 -/
 module
 
+public import Mathlib.Algebra.MvPolynomial.Eval
 public import Mathlib.Algebra.RingQuot
 public import Mathlib.RingTheory.DividedPowers.Basic
 
@@ -16,7 +17,7 @@ the universal divided power algebra of `M`, as the ring quotient of the polynomi
 in the variables `ℕ × M` by the relation `DividedPowerAlgebra.Rel`.
 
 `DividedPowerAlgebra R M` satisfies a weak universal property for morphisms to rings with
-divided powers.
+divided powers (`DividedPowerAlgebra.lift`).
 
 ## Main definitions
 
@@ -35,6 +36,14 @@ divided powers.
 
   The API will be setup so that it is never (never say never…) necessary to lift to `MvPolynomial`.
 
+* `DividedPowerAlgebra.lift`: the weak universal property of `DividedPowerAlgebra R M`.
+
+* `DividedPowerAlgebra.map`: the functoriality map between divided power algebras
+  associated with a linear map of the underlying modules.
+  Given an `R`-algebra `S`, an `S`-module `N` and an `R`-linear map `f : M →ₗ[R] N`,
+  this is the map `DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N`
+  sending `dp R n m` to `dp S n (f m)`.
+
 ## References
 
 * [P. Berthelot (1974), *Cohomologie cristalline des schémas de
@@ -50,7 +59,6 @@ divided powers.
 
 ## TODO
 
-* Add the weak universal property of `DividedPowerAlgebra R M`.
 * Show in upcoming files that `DividedPowerAlgebra R M` has divided powers.
 
 
@@ -73,7 +81,7 @@ inductive Rel : MvPolynomial (ℕ × M) R → MvPolynomial (ℕ × M) R → Prop
   | 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))
+    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)
@@ -132,13 +140,12 @@ protected theorem induction_on' {P : DividedPowerAlgebra R M → Prop} (f : Divi
 protected theorem induction_on {P : DividedPowerAlgebra R M → Prop} (f : DividedPowerAlgebra R M)
     (C : ∀ a, P (algebraMap R _ a)) (add : ∀ f g, P f → P g → P (f + g))
     (dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)) : P f :=
-  DividedPowerAlgebra.induction_on' f (fun a => by rw [mkAlgHom_C]; exact C a) add dp
+  DividedPowerAlgebra.induction_on' f (fun a ↦ by rw [mkAlgHom_C]; exact C a) add dp
 
 theorem dp_eq_mkRingHom (n : ℕ) (m : M) :
     dp R n m = mkRingHom (Rel R M) (X (⟨n, m⟩)) := by
   simp [dp, mkRingHom, mkAlgHom]
 
-@[simp]
 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
@@ -164,22 +171,22 @@ theorem dp_mul {n p : ℕ} {m : M} :
   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
+    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) :=
+      (Finset.sym s q).sum fun k ↦ s.prod fun i ↦ dp R (Multiset.count i k) (x i) :=
   DividedPowers.dpow_sum' (I := ⊤) _ (fun _ ↦ dp_zero)
     (fun _ _ ↦ dp_add) dp_null_of_ne_zero (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
+    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
@@ -220,7 +227,7 @@ theorem algHom_ext_iff {A : Type*} [CommSemiring A] [Algebra R A]
   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
+  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]
@@ -281,4 +288,211 @@ theorem submodule_span_prod_dp_eq_top (hv : span R (Set.range v) = ⊤) :
 
 end
 
+section UniversalProperty
+
+variable (R M)
+
+variable {A : Type*} [CommSemiring A] [Algebra R A]
+
+private theorem lift'_imp {f : ℕ × M → A} (hf_zero : ∀ m, f (0, m) = 1)
+    (hf_smul : ∀ (n : ℕ) (r : R) (m : M), f ⟨n, r • m⟩ = r ^ n • f ⟨n, m⟩)
+    (hf_mul : ∀ n p m, f ⟨n, m⟩ * f ⟨p, m⟩ = (n + p).choose n • f ⟨n + p, m⟩)
+    (hf_add : ∀ n u v, f ⟨n, u + v⟩ = (antidiagonal n).sum fun (k, l) ↦ f ⟨k, u⟩ * f ⟨l, v⟩)
+    (p q : MvPolynomial (ℕ × M) R) (h : (Rel R M) p q) :
+    eval₂AlgHom R f p = eval₂AlgHom R f q := by
+  rcases h <;>
+  simp_all
+
+variable {R M}
+
+/-- The weak universal property of `DividedPowerAlgebra R M`. -/
+def lift' {f : ℕ × M → A} (hf_zero : ∀ m, f (0, m) = 1)
+    (hf_smul : ∀ (n : ℕ) (r : R) (m : M), f ⟨n, r • m⟩ = r ^ n • f ⟨n, m⟩)
+    (hf_mul : ∀ n p m, f ⟨n, m⟩ * f ⟨p, m⟩ = (n + p).choose n • f ⟨n + p, m⟩)
+    (hf_add : ∀ n u v, f ⟨n, u + v⟩ = (antidiagonal n).sum fun (k, l) ↦ f ⟨k, u⟩ * f ⟨l, v⟩) :
+    DividedPowerAlgebra R M →ₐ[R] A :=
+  RingQuot.liftAlgHom R ⟨eval₂AlgHom R f, by exact lift'_imp R M hf_zero hf_smul hf_mul hf_add⟩
+
+@[simp]
+theorem lift'_apply {f : ℕ × M → A} (hf_zero : ∀ m, f (0, m) = 1)
+    (hf_smul : ∀ (n : ℕ) (r : R) (m : M), f ⟨n, r • m⟩ = r ^ n • f ⟨n, m⟩)
+    (hf_mul : ∀ n p m, f ⟨n, m⟩ * f ⟨p, m⟩ = (n + p).choose n • f ⟨n + p, m⟩)
+    (hf_add : ∀ n u v, f ⟨n, u + v⟩ = (antidiagonal n).sum fun (k, l) ↦ f ⟨k, u⟩ * f ⟨l, v⟩)
+    (p : MvPolynomial (ℕ × M) R) :
+    lift' hf_zero hf_smul hf_mul hf_add (mkAlgHom R (Rel R M) p) = aeval f p := by
+  simp [lift', aeval_eq_eval₂Hom]
+
+@[simp]
+theorem lift'_apply_dp {f : ℕ × M → A} (hf_zero : ∀ m, f (0, m) = 1)
+    (hf_smul : ∀ (n : ℕ) (r : R) (m : M), f ⟨n, r • m⟩ = r ^ n • f ⟨n, m⟩)
+    (hf_mul : ∀ n p m, f ⟨n, m⟩ * f ⟨p, m⟩ = (n + p).choose n • f ⟨n + p, m⟩)
+    (hf_add : ∀ n u v, f ⟨n, u + v⟩ = (antidiagonal n).sum fun (k, l) ↦ f ⟨k, u⟩ * f ⟨l, v⟩)
+    (n : ℕ) (m : M) :
+    lift' hf_zero hf_smul hf_mul hf_add (dp R n m) = f ⟨n, m⟩ := by
+  rw [dp_def, lift'_apply hf_zero hf_smul hf_mul hf_add, aeval_X]
+
+variable {I : Ideal A} (hI : DividedPowers I) (g : M →ₗ[R] A) (hg : ∀ m, g m ∈ I)
+
+/-- The weak universal property of a divided power algebra for morphisms to divided power rings -/
+def lift : DividedPowerAlgebra R M →ₐ[R] A :=
+  lift' (f := fun nm ↦ hI.dpow nm.1 (g nm.2))
+    (fun m ↦ hI.dpow_zero (hg m))
+    (fun n r m ↦ by
+      dsimp only
+      rw [LinearMap.map_smulₛₗ, RingHom.id_apply, ← algebraMap_smul A r (g m), smul_eq_mul,
+        hI.dpow_mul (hg m), ← smul_eq_mul, ← map_pow, algebraMap_smul])
+    (fun n p m ↦ by rw [hI.mul_dpow (hg m), ← nsmul_eq_mul])
+    (fun n u v ↦ by simp [hI.dpow_add (hg u) (hg v)])
+
+variable {g}
+
+@[simp]
+theorem lift_apply (p : MvPolynomial (ℕ × M) R) :
+    lift hI g hg (mkAlgHom R (Rel R M) p) = aeval (fun nm : ℕ × M ↦ hI.dpow nm.1 (g nm.2)) p := by
+  rw [lift, lift'_apply]
+
+@[simp]
+theorem lift_apply_dp (n : ℕ) (m : M) :
+    lift hI g hg (dp R n m) = hI.dpow n (g m) := by rw [lift, lift'_apply_dp]
+
+theorem lift_unique {f : DividedPowerAlgebra R M →ₐ[R] A}
+    (hf : ∀ n m, f (dp R n m) = hI.dpow n (g m)) : f = lift hI g hg :=
+  algHom_ext (fun _ _ ↦ by rw [lift_apply_dp, hf])
+
+@[simp]
+theorem lift_embed_apply (m : M) : lift hI g hg (embed R M m) = g m := by
+  simp [embed_def, hI.dpow_one (hg m)]
+
+@[simp]
+theorem embed_comp_lift : (lift hI g hg).toLinearMap.comp (embed R M) = g := by
+  ext; simp
+
+end UniversalProperty
+
+section Functoriality
+
+section Map
+
+variable {S : Type*} [CommSemiring S] {N : Type*} [AddCommMonoid N] [Module R N] [Module S N]
+  (f : M →ₗ[R] N)
+
+namespace LinearMap
+
+@[simp]
+lemma dp_zero {a : M} : dp S 0 (f a) = 1 := DividedPowerAlgebra.dp_zero
+
+lemma dp_mul {m n : ℕ} {a : M} :
+    dp S m (f a) * dp S n (f a) = (Nat.choose (m + n) m) • dp S (m + n) (f a) :=
+  DividedPowerAlgebra.dp_mul
+
+lemma dp_add {n : ℕ} {a b : M} :
+    dp S n (f (a + b)) = (Finset.antidiagonal n).sum fun k ↦ dp S k.1 (f a) * dp S k.2 (f b) := by
+  rw [map_add, DividedPowerAlgebra.dp_add]
+
+end LinearMap
+
+section IsScalarTower
+
+variable (S)
+
+variable [Algebra R S] [IsScalarTower R S N]
+
+lemma LinearMap.dp_smul {n : ℕ} {r : R} {a : M} : dp S n (f (r • a)) = r ^ n • dp S n (f a) := by
+  rw [f.map_smul, algebra_compatible_smul S r (f a),
+    DividedPowerAlgebra.dp_smul, ← map_pow, algebraMap_smul]
+
+/-- The functoriality map between divided power algebras associated with a linear map of the
+  underlying modules.
+  Given an `R`-algebra `S`, an `S`-module `N` and an `R`-linear map `f : M →ₗ[R] N`,
+  this is the map `DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N`
+  sending `dp R n m` to `dp S n (f m)`. -/
+def map : DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N :=
+  DividedPowerAlgebra.lift' (f := fun nm ↦ dp S nm.fst (f nm.snd))
+    (fun _ ↦ LinearMap.dp_zero f)
+    (fun _ _ _ ↦ LinearMap.dp_smul S f)
+    (fun _ _ _ ↦ LinearMap.dp_mul f)
+    (fun _ _ _ ↦ LinearMap.dp_add f)
+
+@[simp]
+theorem map_apply {p : MvPolynomial (ℕ × M) R} :
+    map S f (mkAlgHom R (Rel R M) p) = aeval (fun nm ↦ dp S nm.fst (f nm.snd)) p := by
+  rw [map, lift'_apply]
+
+@[simp]
+theorem map_apply_dp {n : ℕ} {a : M} : map S f (dp R n a) = dp S n (f a) := by
+  rw [map, lift'_apply_dp]
+
+@[simp]
+theorem map_embed_apply {m : M} : map S f (embed R M m) = embed S N (f m) := by
+  simp [embed_def, map_apply_dp]
+
+theorem lift_comp_embed :
+    (map S f).toLinearMap.comp (embed R M) = ((embed S N).restrictScalars R).comp f := by
+  ext; simp
+
+theorem lift_surjective {f : M →ₗ[R] N} (hf : Function.Surjective f) :
+    Function.Surjective (map R f) := by
+  rw [← AlgHom.range_eq_top, ← Algebra.map_top (map R f), eq_top_iff,
+    ← (AlgHom.range_eq_top (mkAlgHom R (Rel R N))).mpr mkAlgHom_surjective,
+    ← Algebra.map_top, (Subalgebra.gc_map_comap _).le_iff_le, ← MvPolynomial.adjoin_range_X,
+    Algebra.adjoin_le_iff]
+  intro
+  simp only [Set.mem_range, Prod.exists]
+  rintro ⟨n, m, rfl⟩
+  obtain ⟨l, rfl⟩ := hf m
+  simp only [Algebra.map_top, Subalgebra.coe_comap, AlgHom.coe_range, Set.mem_preimage,
+    Set.mem_range]
+  use dp R n l
+  rw [map_apply_dp, dp]
+
+end IsScalarTower
+
+end Map
+
+variable (S : Type*) [CommSemiring S] {N : Type*} [AddCommMonoid N] [Module R N] [Module S N]
+  (f : M →ₗ[R] N)
+
+section IsScalarTower
+
+variable [Algebra R S] [IsScalarTower R S N] {P : Type*} [AddCommMonoid P] [Module R P]
+
+lemma map_comp (f : M →ₗ[R] N) (g : N →ₗ[R] P) :
+    map R (g.comp f) = (map R g).comp (map R f) := by
+  rw [algHom_ext_iff]
+  intros; simp [map_apply_dp]
+
+@[simp]
+lemma map_id : map R (LinearMap.id (R := R) (M := M)) = AlgHom.id R _ := by
+  rw [algHom_ext_iff]
+  intros
+  simp [map_apply_dp]
+
+/-- The functoriality map between divided power algebras associated with a linear equivalence of
+  the underlying modules. Given an `R`-algebra `S`, an `S`-module `N` and an `R`-linear equivalence
+  `f : M →ₗ[R] N`, this is the map `DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N`
+  sending `dp R n m` to `dp S n (f m)`. -/
+@[simps!]
+def mapEquiv (g : M ≃ₗ[R] N) :
+    DividedPowerAlgebra R M ≃ₐ[R] DividedPowerAlgebra R N :=
+  AlgEquiv.ofAlgHom (map R g.toLinearMap) (map R g.symm.toLinearMap)
+    (by simp [← map_comp, map_id]) (by simp [← map_comp, map_id])
+
+theorem mapEquiv_symm (g : M ≃ₗ[R] N) : (mapEquiv g).symm = mapEquiv g.symm := rfl
+
+theorem LinearEquiv.coe_lift (g : M ≃ₗ[R] N) : mapEquiv g = map R g.toLinearMap := rfl
+
+theorem LinearEquiv.coe_lift_symm (g : M ≃ₗ[R] N) :
+    (mapEquiv g).symm = map R g.symm.toLinearMap := rfl
+
+theorem mapEquiv_refl : mapEquiv (LinearEquiv.refl R M) = AlgEquiv.refl :=
+  AlgEquiv.coe_algHom_injective map_id
+
+theorem mapEquiv_trans (g : M ≃ₗ[R] N) (h : N ≃ₗ[R] P) :
+    (mapEquiv g).trans (mapEquiv h) = mapEquiv (g.trans h) :=
+  AlgEquiv.coe_algHom_injective (map_comp _ _).symm
+
+end IsScalarTower
+
+end Functoriality
+
 end DividedPowerAlgebra