The augmentation of a divided power algebra

For a module M over a commutative semiring R, the divided power algebra Γ_R(M) carries a canonical R-algebra map ε : Γ_R(M) → R, the augmentation, sending dp R 0 m to 1 and every dp R n m with n > 0 to 0. It is the lift of the zero linear map M → R into the zero ideal of R, equipped with its canonical divided powers. Its kernel is the augmentation ideal Γ_R(M)₊, the ideal on which the divided powers of Γ_R(M) live; it is the input to divided power envelopes and crystalline constructions.

Over a commutative semiring, Γ_R(M)₊ is the ideal generated by the positive divided powers dp R n m, n > 0. The degree-one generators dp R 1 m do not suffice in general: over ZMod 2, an ordinary algebra map to the dual numbers detects dp 2 1 and kills every dp 1 m.

Over a commutative ring, Γ_R(M) splits as R × Γ_R(M)₊, and for every ideal I of R the extended ideal IΓ meets Γ_R(M)₊ exactly in IΓ · Γ_R(M)₊. These are instances of the general facts about the kernel of an augmentation A →ₐ[R] R in TauCeti.RingTheory.Ideal.IsAugmentation, stated here for the augmentation ideal.

No freeness, finiteness or characteristic hypothesis is imposed on M.

Main declarations

• DividedPowerAlgebra.augmentation: the augmentation Γ_R(M) →ₐ[R] R.
• DividedPowerAlgebra.augmentation_dp: its value on the generators dp R n m.
• DividedPowerAlgebra.augmentation_map: compatibility with DividedPowerAlgebra.map.
• DividedPowerAlgebra.augmentation_unique: an algebra map to R killing the positive generators is the augmentation.
• DividedPowerAlgebra.augmentationIdeal: the augmentation ideal Γ_R(M)₊.
• DividedPowerAlgebra.augmentationIdeal_eq_span: Γ_R(M)₊ is generated by the dp R n m with n ≠ 0.
• DividedPowerAlgebra.augmentationSplitting: the R-linear splitting Γ_R(M) ≃ R × Γ_R(M)₊.
• DividedPowerAlgebra.map_algebraMap_inf_augmentationIdeal_eq_mul: IΓ ∩ Γ_R(M)₊ = IΓ · Γ_R(M)₊ for every ideal I of R.
• DividedPowerAlgebra.dp_two_not_mem_span_dp_one: in Γ_{𝔽₂}(𝔽₂), dp 2 1 is not in the ideal generated by the degree-one elements.

References

• Mathlib's DividedPowerAlgebra and dividedPowersBot, from the divided powers formalization of A. Chambert-Loir and M. I. de Frutos-Fernández; the augmentation is their lift along the zero map.
• N. Roby, Lois polynomes et lois formelles en théorie des modules, Ann. Sci. ÉNS 80 (1963), III §§1–2.
• Stacks: Divided power algebra, Tag 07H4 and Lemma 07H5.

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

The augmentation Γ_R(M) →ₐ[R] R of the divided power algebra, sending dp R 0 m to 1 and dp R n m to 0 for n ≠ 0. It is the lift of the zero map M → R into the zero ideal of R with its canonical divided powers.

theorem DividedPowerAlgebra.augmentation_eq_lift (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : augmentation R M = lift (dividedPowersBot R) 0 ⋯

@[simp]

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

The augmentation is 1 on dp R 0 m and 0 on every dp R n m with n ≠ 0.

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

theorem DividedPowerAlgebra.augmentation_surjective {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Function.Surjective ⇑(augmentation R M)

The augmentation is surjective, being a retraction of algebraMap R (Γ_R(M)).

theorem DividedPowerAlgebra.augmentation_unique {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f : DividedPowerAlgebra R M →ₐ[R] R} (hf : ∀ (n : ℕ) (m : M), n ≠ 0 → f (dp R n m) = 0) : f = augmentation R M

An R-algebra map Γ_R(M) → R killing every dp R n m with n ≠ 0 is the augmentation.

theorem DividedPowerAlgebra.augmentation_comp_map {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) : (AlgHom.restrictScalars R (augmentation S N)).comp (map S f) = (Algebra.ofId R S).comp (augmentation R M)

The augmentation is natural: ε_S ∘ Γ(f) = algebraMap R S ∘ ε_R.

@[simp]

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

Elementwise naturality of the augmentation along DividedPowerAlgebra.map.

noncomputable def DividedPowerAlgebra.augmentationIdeal (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Ideal (DividedPowerAlgebra R M)

The augmentation ideal Γ_R(M)₊ of the divided power algebra, the kernel of the augmentation.

theorem DividedPowerAlgebra.augmentationIdeal_eq_ker (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : augmentationIdeal R M = RingHom.ker (augmentation R M)

@[simp]

theorem DividedPowerAlgebra.mem_augmentationIdeal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {z : DividedPowerAlgebra R M} : z ∈ augmentationIdeal R M ↔ (augmentation R M) z = 0

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

theorem DividedPowerAlgebra.algebraMap_mem_augmentationIdeal_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {r : R} : (algebraMap R (DividedPowerAlgebra R M)) r ∈ augmentationIdeal R M ↔ r = 0

A scalar lies in the augmentation ideal exactly when it is zero.

theorem DividedPowerAlgebra.augmentationIdeal_ne_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] : augmentationIdeal R M ≠ ⊤

Over a nontrivial ring the augmentation ideal is proper.

theorem DividedPowerAlgebra.map_mem_augmentationIdeal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} [CommSemiring S] [Algebra R S] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) {z : DividedPowerAlgebra R M} (hz : z ∈ augmentationIdeal R M) : (map S f) z ∈ augmentationIdeal S N

The map Γ(f) carries the augmentation ideal into the augmentation ideal.

theorem DividedPowerAlgebra.augmentationIdeal_eq_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : augmentationIdeal R M = Ideal.span {x : DividedPowerAlgebra R M | ∃ (n : ℕ) (m : M), n ≠ 0 ∧ dp R n m = x}

The augmentation ideal is generated by the positive divided powers dp R n m, n ≠ 0.

theorem DividedPowerAlgebra.sub_algebraMap_augmentation_mem_span {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (z : DividedPowerAlgebra R M) : z - (algebraMap R (DividedPowerAlgebra R M)) ((augmentation R M) z) ∈ Ideal.span {x : DividedPowerAlgebra R M | ∃ (n : ℕ) (m : M), n ≠ 0 ∧ dp R n m = x}

Every element differs from the scalar given by its augmentation by an element of the ideal generated by the positive divided powers dp R n m, n ≠ 0.

noncomputable def DividedPowerAlgebra.augmentationSplitting (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommMonoid M] [Module R M] : DividedPowerAlgebra R M ≃ₗ[R] R × ↥(augmentationIdeal R M)

The splitting of Γ_R(M) into scalars and the augmentation ideal, as R-modules: z ↦ (ε z, z - algebraMap R _ (ε z)), with inverse (r, u) ↦ algebraMap R _ r + u.

@[simp]

theorem DividedPowerAlgebra.augmentationSplitting_apply_fst {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (z : DividedPowerAlgebra R M) : ((augmentationSplitting R M) z).1 = (augmentation R M) z

@[simp]

theorem DividedPowerAlgebra.coe_augmentationSplitting_apply_snd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (z : DividedPowerAlgebra R M) : ↑((augmentationSplitting R M) z).2 = z - (algebraMap R (DividedPowerAlgebra R M)) ((augmentation R M) z)

@[simp]

theorem DividedPowerAlgebra.augmentationSplitting_symm_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (p : R × ↥(augmentationIdeal R M)) : (augmentationSplitting R M).symm p = (algebraMap R (DividedPowerAlgebra R M)) p.1 + ↑p.2

theorem DividedPowerAlgebra.sub_algebraMap_augmentation_mem_map_mul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] {I : Ideal R} {z : DividedPowerAlgebra R M} (hz : z ∈ Ideal.map (algebraMap R (DividedPowerAlgebra R M)) I) : z - (algebraMap R (DividedPowerAlgebra R M)) ((augmentation R M) z) ∈ Ideal.map (algebraMap R (DividedPowerAlgebra R M)) I * augmentationIdeal R M

For an ideal I of R, the remainder z - algebraMap R _ (ε z) of an element z of the extended ideal IΓ lies in IΓ · Γ_R(M)₊.

theorem DividedPowerAlgebra.map_algebraMap_inf_augmentationIdeal_eq_mul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (I : Ideal R) : Ideal.map (algebraMap R (DividedPowerAlgebra R M)) I ⊓ augmentationIdeal R M = Ideal.map (algebraMap R (DividedPowerAlgebra R M)) I * augmentationIdeal R M

For an ideal I of R, the extended ideal IΓ meets the augmentation ideal exactly in IΓ · Γ_R(M)₊.

theorem DividedPowerAlgebra.exists_algHom_trivSqZeroExt_dp : ∃ (f : DividedPowerAlgebra (ZMod 2) (ZMod 2) →ₐ[ZMod 2] TrivSqZeroExt (ZMod 2) (ZMod 2)), ∀ (n : ℕ) (a : ZMod 2), f (dp (ZMod 2) n a) = if n = 0 then 1 else if n = 2 then TrivSqZeroExt.inr a else 0

In characteristic two there is an ordinary algebra map Γ_{𝔽₂}(𝔽₂) → 𝔽₂[ε] to the dual numbers sending dp 0 a to 1, dp 2 a to inr a, and every other dp n a to 0.

theorem DividedPowerAlgebra.dp_two_not_mem_span_dp_one : dp (ZMod 2) 2 1 ∉ Ideal.span (Set.range fun (m : ZMod 2) => dp (ZMod 2) 1 m)

The degree-one elements do not generate the augmentation ideal: in Γ_{𝔽₂}(𝔽₂), dp 2 1 is not in the ideal generated by the dp 1 m.