The universal divided power algebra

Let R be a (commutative) semiring 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 (DividedPowerAlgebra.lift).

Main definitions

• DividedPowerAlgebra.Rel: the type coding the basic relations that will give rise to the divided power algebra.

• DividedPowerAlgebra R M: the universal divided power algebra of the R-module M, defined as RingQuot of DividedPowerAlgebra.Rel R M.

• DividedPowerAlgebra.dp R n m: for n : ℕ and m : M, this is the equivalence class of MvPolynomial.X (⟨n, m⟩) in DividedPowerAlgebra R M.

  When that algebra is endowed with its canonical divided power structure (to be defined), the image of MvPolynomial.X (n, m), for any n : ℕ and m : M, is equal to the nth divided power of the image of m.

  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 caractéristique $p$ > 0

• P. Berthelot and A. Ogus (1978), Notes on crystalline cohomology

• N. Roby (1963), Lois polynomes et lois formelles en théorie des modules

• N. Roby (1965), Les algèbres à puissances dividées

TODO

• Show in upcoming files that DividedPowerAlgebra R M has divided powers.

inductive DividedPowerAlgebra.Rel (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : MvPolynomial (ℕ × M) R → MvPolynomial (ℕ × M) R → Prop

The type coding the basic relations that will give rise to the divided power algebra. The class of MvPolynomial.X (n, a) will be equal to dpow n a, for a ∈ M.

• rfl_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Rel R M 0 0
• zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {a : M} : Rel R M (MvPolynomial.X (0, a)) 1
• smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {r : R} {n : ℕ} {a : M} : Rel R M (MvPolynomial.X (n, r • a)) (r ^ n • MvPolynomial.X (n, a))
• mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {m n : ℕ} {a : M} : Rel R M (MvPolynomial.X (m, a) * MvPolynomial.X (n, a)) ((m + n).choose m • MvPolynomial.X (m + n, a))
• add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} {a b : M} : Rel R M (MvPolynomial.X (n, a + b)) (∑ k ∈ Finset.antidiagonal n, MvPolynomial.X (k.1, a) * MvPolynomial.X (k.2, b))

noncomputable def DividedPowerAlgebra.RelI (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Ideal (MvPolynomial (ℕ × M) R)

The ideal of MvPolynomial (ℕ × M) R generated by Rel.

Equations

• DividedPowerAlgebra.RelI R M = Ideal.ofRel (DividedPowerAlgebra.Rel R M)

@[reducible, inline]

abbrev DividedPowerAlgebra (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max u_1 u_2)

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.

Equations

• DividedPowerAlgebra R M = RingQuot (DividedPowerAlgebra.Rel R M)

theorem DividedPowerAlgebra.mkAlgHom_surjective {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Function.Surjective ⇑(RingQuot.mkAlgHom R (Rel R M))

theorem DividedPowerAlgebra.mkAlgHom_C {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : (RingQuot.mkAlgHom R (Rel R M)) (MvPolynomial.C a) = (algebraMap R (DividedPowerAlgebra R M)) a

theorem DividedPowerAlgebra.mkRingHom_C {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : (RingQuot.mkRingHom (Rel R M)) (MvPolynomial.C a) = (algebraMap R (DividedPowerAlgebra R M)) a

noncomputable def DividedPowerAlgebra.dp (R : Type u_1) {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : M) : DividedPowerAlgebra R M

dp R n m is the equivalence class of X (⟨n, m⟩) in DividedPowerAlgebra R M.

Equations

• DividedPowerAlgebra.dp R n m = (RingQuot.mkAlgHom R (DividedPowerAlgebra.Rel R M)) (MvPolynomial.X (n, m))

theorem DividedPowerAlgebra.dp_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : M) : dp R n m = (RingQuot.mkAlgHom R (Rel R M)) (MvPolynomial.X (n, m))

theorem DividedPowerAlgebra.induction_on' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {P : DividedPowerAlgebra R M → Prop} (f : DividedPowerAlgebra R M) (h_C : ∀ (a : R), P ((RingQuot.mkAlgHom R (Rel R M)) (MvPolynomial.C a))) (h_add : ∀ (f g : DividedPowerAlgebra R M), 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

theorem DividedPowerAlgebra.induction_on {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {P : DividedPowerAlgebra R M → Prop} (f : DividedPowerAlgebra R M) (C : ∀ (a : R), P ((algebraMap R (DividedPowerAlgebra R M)) a)) (add : ∀ (f g : DividedPowerAlgebra R M), 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

theorem DividedPowerAlgebra.dp_eq_mkRingHom {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : M) : dp R n m = (RingQuot.mkRingHom (Rel R M)) (MvPolynomial.X (n, m))

theorem DividedPowerAlgebra.dp_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {m : M} : dp R 0 m = 1

theorem DividedPowerAlgebra.dp_smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {r : R} {n : ℕ} {m : M} : dp R n (r • m) = r ^ n • dp R n m

theorem DividedPowerAlgebra.dp_null {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} : dp R n 0 = if n = 0 then 1 else 0

theorem DividedPowerAlgebra.dp_null_of_ne_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (hn : n ≠ 0) : dp R n 0 = 0

theorem DividedPowerAlgebra.dp_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n p : ℕ} {m : M} : dp R n m * dp R p m = (n + p).choose n • dp R (n + p) m

theorem DividedPowerAlgebra.dp_add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} {x y : M} : dp R n (x + y) = ∑ k ∈ Finset.antidiagonal n, dp R k.1 x * dp R k.2 y

theorem DividedPowerAlgebra.dp_sum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [DecidableEq ι] (s : Finset ι) (q : ℕ) (x : ι → M) : dp R q (s.sum x) = ∑ k ∈ s.sym q, ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)

theorem DividedPowerAlgebra.dp_sum_smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [DecidableEq ι] (s : Finset ι) (q : ℕ) (a : ι → R) (x : ι → M) : dp R q (∑ i ∈ s, a i • x i) = ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)

theorem DividedPowerAlgebra.prod_dp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {s : Finset ι} {n : ι → ℕ} {m : M} : ∏ i ∈ s, dp R (n i) m = ↑(Nat.multinomial s n) * dp R (s.sum n) m

theorem DividedPowerAlgebra.natFactorial_mul_dp_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : M) : ↑n.factorial * dp R n x = dp R 1 x ^ n

noncomputable def DividedPowerAlgebra.embed (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] DividedPowerAlgebra R M

The canonical linear map M →ₗ[R] DividedPowerAlgebra R M.

Equations

• DividedPowerAlgebra.embed R M = { toFun := fun (m : M) => DividedPowerAlgebra.dp R 1 m, map_add' := ⋯, map_smul' := ⋯ }

theorem DividedPowerAlgebra.embed_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) : (embed R M) m = dp R 1 m

theorem DividedPowerAlgebra.algHom_ext_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {f g : DividedPowerAlgebra R M →ₐ[R] A} : f = g ↔ ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

theorem DividedPowerAlgebra.algHom_ext {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {f g : DividedPowerAlgebra R M →ₐ[R] A} (h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) : f = g

theorem DividedPowerAlgebra.submodule_span_prod_dp_eq_top {R : Type u_3} {M : Type u_4} {ι : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) : Submodule.span R (Set.range fun (n : ι →₀ ℕ) => n.prod fun (i : ι) (k : ℕ) => dp R k (v i)) = ⊤

theorem DividedPowerAlgebra.pow_dp {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) (m : M) (k : ℕ) : dp R n m ^ k = ↑(k • {n}).multinomial * dp R (k * n) m

noncomputable def DividedPowerAlgebra.lift' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {f : ℕ × M → A} (hf_zero : ∀ (m : 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 : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)) (hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ Finset.antidiagonal n, match x with | (k, l) => f (k, u) * f (l, v)) : DividedPowerAlgebra R M →ₐ[R] A

The weak universal property of DividedPowerAlgebra R M.

Equations

• DividedPowerAlgebra.lift' hf_zero hf_smul hf_mul hf_add = (RingQuot.liftAlgHom R) ⟨MvPolynomial.eval₂AlgHom R f, ⋯⟩

@[simp]

theorem DividedPowerAlgebra.lift'_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {f : ℕ × M → A} (hf_zero : ∀ (m : 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 : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)) (hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ Finset.antidiagonal n, match x with | (k, l) => f (k, u) * f (l, v)) (p : MvPolynomial (ℕ × M) R) : (lift' hf_zero hf_smul hf_mul hf_add) ((RingQuot.mkAlgHom R (Rel R M)) p) = (MvPolynomial.aeval f) p

@[simp]

theorem DividedPowerAlgebra.lift'_apply_dp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {f : ℕ × M → A} (hf_zero : ∀ (m : 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 : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)) (hf_add : ∀ (n : ℕ) (u v : M), f (n, u + v) = ∑ x ∈ Finset.antidiagonal n, match x with | (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)

noncomputable def DividedPowerAlgebra.lift {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {I : Ideal A} (hI : DividedPowers I) (g : M →ₗ[R] A) (hg : ∀ (m : M), g m ∈ I) : DividedPowerAlgebra R M →ₐ[R] A

The weak universal property of a divided power algebra for morphisms to divided power rings

Equations

• DividedPowerAlgebra.lift hI g hg = DividedPowerAlgebra.lift' ⋯ ⋯ ⋯ ⋯

@[simp]

theorem DividedPowerAlgebra.lift_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A} (hg : ∀ (m : M), g m ∈ I) (p : MvPolynomial (ℕ × M) R) : (lift hI g hg) ((RingQuot.mkAlgHom R (Rel R M)) p) = (MvPolynomial.aeval fun (nm : ℕ × M) => hI.dpow nm.1 (g nm.2)) p

@[simp]

theorem DividedPowerAlgebra.lift_apply_dp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A} (hg : ∀ (m : M), g m ∈ I) (n : ℕ) (m : M) : (lift hI g hg) (dp R n m) = hI.dpow n (g m)

theorem DividedPowerAlgebra.lift_unique {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A} (hg : ∀ (m : M), g m ∈ I) {f : DividedPowerAlgebra R M →ₐ[R] A} (hf : ∀ (n : ℕ) (m : M), f (dp R n m) = hI.dpow n (g m)) : f = lift hI g hg

@[simp]

theorem DividedPowerAlgebra.lift_embed_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A} (hg : ∀ (m : M), g m ∈ I) (m : M) : (lift hI g hg) ((embed R M) m) = g m

@[simp]

theorem DividedPowerAlgebra.embed_comp_lift {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A} (hg : ∀ (m : M), g m ∈ I) : (lift hI g hg).toLinearMap ∘ₗ embed R M = g

@[simp]

theorem DividedPowerAlgebra.LinearMap.dp_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] (f : M →ₗ[R] N) {a : M} : dp S 0 (f a) = 1

theorem DividedPowerAlgebra.LinearMap.dp_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] (f : M →ₗ[R] N) {m n : ℕ} {a : M} : dp S m (f a) * dp S n (f a) = (m + n).choose m • dp S (m + n) (f a)

theorem DividedPowerAlgebra.LinearMap.dp_add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] (f : M →ₗ[R] N) {n : ℕ} {a b : M} : dp S n (f (a + b)) = ∑ k ∈ Finset.antidiagonal n, dp S k.1 (f a) * dp S k.2 (f b)

theorem DividedPowerAlgebra.LinearMap.dp_smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] (f : M →ₗ[R] N) [Algebra R S] [IsScalarTower R S N] {n : ℕ} {r : R} {a : M} : dp S n (f (r • a)) = r ^ n • dp S n (f a)

noncomputable def DividedPowerAlgebra.map {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] (f : M →ₗ[R] N) [Algebra R S] [IsScalarTower R S N] : DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N

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).

Equations

• DividedPowerAlgebra.map S f = DividedPowerAlgebra.lift' ⋯ ⋯ ⋯ ⋯

@[simp]

theorem DividedPowerAlgebra.map_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] (f : M →ₗ[R] N) [Algebra R S] [IsScalarTower R S N] {p : MvPolynomial (ℕ × M) R} : (map S f) ((RingQuot.mkAlgHom R (Rel R M)) p) = (MvPolynomial.aeval fun (nm : ℕ × M) => dp S nm.1 (f nm.2)) p

@[simp]

theorem DividedPowerAlgebra.map_apply_dp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] (f : M →ₗ[R] N) [Algebra R S] [IsScalarTower R S N] {n : ℕ} {a : M} : (map S f) (dp R n a) = dp S n (f a)

@[simp]

theorem DividedPowerAlgebra.map_embed_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] (f : M →ₗ[R] N) [Algebra R S] [IsScalarTower R S N] {m : M} : (map S f) ((embed R M) m) = (embed S N) (f m)

theorem DividedPowerAlgebra.lift_comp_embed {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_3) [CommSemiring S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] (f : M →ₗ[R] N) [Algebra R S] [IsScalarTower R S N] : (map S f).toLinearMap ∘ₗ embed R M = ↑R (embed S N) ∘ₗ f

theorem DividedPowerAlgebra.lift_surjective {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(map R f)

theorem DividedPowerAlgebra.map_comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_5} [AddCommMonoid P] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : map R (g ∘ₗ f) = (map R g).comp (map R f)

@[simp]

theorem DividedPowerAlgebra.map_id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : map R LinearMap.id = AlgHom.id R (DividedPowerAlgebra R M)

noncomputable def DividedPowerAlgebra.mapEquiv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (g : M ≃ₗ[R] N) : DividedPowerAlgebra R M ≃ₐ[R] DividedPowerAlgebra R N

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).

Equations

• DividedPowerAlgebra.mapEquiv g = AlgEquiv.ofAlgHom (DividedPowerAlgebra.map R ↑g) (DividedPowerAlgebra.map R ↑g.symm) ⋯ ⋯

@[simp]

theorem DividedPowerAlgebra.mapEquiv_symm_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (g : M ≃ₗ[R] N) (a : DividedPowerAlgebra R N) : (mapEquiv g).symm a = (map R ↑g.symm) a

@[simp]

theorem DividedPowerAlgebra.mapEquiv_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (g : M ≃ₗ[R] N) (a : DividedPowerAlgebra R M) : (mapEquiv g) a = (map R ↑g) a

theorem DividedPowerAlgebra.mapEquiv_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (g : M ≃ₗ[R] N) : (mapEquiv g).symm = mapEquiv g.symm

theorem DividedPowerAlgebra.LinearEquiv.coe_lift {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (g : M ≃ₗ[R] N) : ↑(mapEquiv g) = map R ↑g

theorem DividedPowerAlgebra.LinearEquiv.coe_lift_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (g : M ≃ₗ[R] N) : ↑(mapEquiv g).symm = map R ↑g.symm

theorem DividedPowerAlgebra.mapEquiv_refl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : mapEquiv (LinearEquiv.refl R M) = AlgEquiv.refl

theorem DividedPowerAlgebra.mapEquiv_trans {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] {P : Type u_5} [AddCommMonoid P] [Module R P] (g : M ≃ₗ[R] N) (h : N ≃ₗ[R] P) : (mapEquiv g).trans (mapEquiv h) = mapEquiv (g ≪≫ₗ h)