The kernel of an augmentation A →ₐ[R] R

Let A be an algebra, not necessarily commutative, over a commutative ring R, and let ε : A →ₐ[R] R be an R-algebra map, that is, a retraction of algebraMap R A. Its kernel A₊ = ker ε is the augmentation ideal of A. This file records the structure every such kernel has, with no flatness, freeness or finiteness hypothesis:

• every x : A splits as the scalar algebraMap R A (ε x) plus the element x - algebraMap R A (ε x) of A₊, so A₊ is a complement of the scalars in Mathlib's sense Ideal.IsAugmentation, and A ≃ₗ[R] R × A₊;
• for every ideal I of R, with extension IA = I.map (algebraMap R A), the remainder x - algebraMap R A (ε x) of an element x ∈ IA lies in IA * A₊, and hence IA ⊓ A₊ = IA * A₊;
• for commutative A, if A₊ is generated by elements tⱼ, then the quotients A₊ ^ n / A₊ ^ (n + 1) are spanned over R by the monomials of degree n in the tⱼ, and A acts on N / A₊ • N through ε for every A-module N.

The identity IA ⊓ A₊ = IA * A₊ is the compatibility condition between the divided powers of an augmentation ideal and the base ideal I, used for divided-power algebras and divided-power envelopes.

Main declarations

• AlgHom.sub_algebraMap_apply_mem_ker: x - algebraMap R A (ε x) ∈ ker ε.
• AlgHom.isAugmentation_ker: ker ε is an augmentation ideal.
• AlgHom.equivProdKer: the R-linear splitting A ≃ₗ[R] R × ker ε, x ↦ (ε x, x - algebraMap R A (ε x)).
• AlgHom.sub_algebraMap_apply_mem_map_mul_ker: the remainder of x ∈ IA lies in IA * ker ε.
• AlgHom.map_algebraMap_inf_ker_eq_mul: IA ⊓ ker ε = IA * ker ε.
• AlgHom.exists_sub_mem_pow_succ: for commutative A, if ker ε is generated by elements tⱼ, then modulo (ker ε) ^ (n + 1) every element of (ker ε) ^ n is an R-linear combination of the monomials of degree n in the tⱼ.
• AlgHom.smul_sub_smul_mem_smul_top: on an A-module N, a • x - ε a • x ∈ ker ε • N.

References

• Stacks: Divided power algebra, Lemma 07H5, whose proof contains the intersection identity for free modules.
• N. Roby, Lois polynomes et lois formelles en théorie des modules, Ann. Sci. ÉNS 80 (1963), III §§1–2.

theorem AlgHom.sub_algebraMap_apply_mem_ker {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (ε : A →ₐ[R] R) (x : A) : x - (algebraMap R A) (ε x) ∈ RingHom.ker ε

An element differs from the scalar given by its augmentation by an element of the kernel.

theorem AlgHom.isAugmentation_ker {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (ε : A →ₐ[R] R) : Ideal.IsAugmentation R (RingHom.ker ε)

The kernel of an R-algebra map A →ₐ[R] R is a complement of the scalars 1 : Submodule R A, that is, an augmentation ideal.

noncomputable def AlgHom.equivProdKer {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (ε : A →ₐ[R] R) : A ≃ₗ[R] R × ↥(RingHom.ker ε)

The splitting of A into scalars and the kernel of ε, as R-modules: x ↦ (ε x, x - algebraMap R A (ε x)), with inverse (r, u) ↦ algebraMap R A r + u. The multiplication of A is not a product: (algebraMap r + u) * (algebraMap s + v) has the cross terms r • v + s • u.

@[simp]

theorem AlgHom.equivProdKer_apply_fst {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (ε : A →ₐ[R] R) (x : A) : (ε.equivProdKer x).1 = ε x

@[simp]

theorem AlgHom.coe_equivProdKer_apply_snd {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (ε : A →ₐ[R] R) (x : A) : ↑(ε.equivProdKer x).2 = x - (algebraMap R A) (ε x)

@[simp]

theorem AlgHom.equivProdKer_symm_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (ε : A →ₐ[R] R) (p : R × ↥(RingHom.ker ε)) : ε.equivProdKer.symm p = (algebraMap R A) p.1 + ↑p.2

theorem AlgHom.sub_algebraMap_apply_mem_map_mul_ker {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (ε : A →ₐ[R] R) {I : Ideal R} {x : A} (hx : x ∈ Ideal.map (algebraMap R A) I) : x - (algebraMap R A) (ε x) ∈ Ideal.map (algebraMap R A) I * RingHom.ker ε

Remainder of an extended base ideal. For an ideal I of R, the remainder x - algebraMap R A (ε x) of an element x of the extended ideal IA = I.map (algebraMap R A) lies in the product IA * ker ε.

theorem AlgHom.map_algebraMap_inf_ker_eq_mul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (ε : A →ₐ[R] R) (I : Ideal R) : Ideal.map (algebraMap R A) I ⊓ RingHom.ker ε = Ideal.map (algebraMap R A) I * RingHom.ker ε

Base ideal and augmentation intersection. For an ideal I of R, the extended ideal IA = I.map (algebraMap R A) meets the kernel of ε exactly in the product IA * ker ε.

theorem AlgHom.exists_sub_mem_pow_succ {R : Type u_3} {A : Type u_4} [CommRing R] [CommRing A] [Algebra R A] (χ : A →ₐ[R] R) {ι : Type u_5} [Fintype ι] {t : ι → A} (ht : ∀ (j : ι), χ (t j) = 0) (hI : RingHom.ker χ ≤ Ideal.span (Set.range t)) (n : ℕ) {g : A} (hg : g ∈ RingHom.ker χ ^ n) : ∃ q ∈ Submodule.span R {a : A | ∃ (β : ι → ℕ), ∑ j : ι, β j = n ∧ ∏ j : ι, t j ^ β j = a}, g - q ∈ RingHom.ker χ ^ (n + 1)

If the kernel of χ : A →ₐ[R] R is generated by elements tⱼ vanishing at χ, then every element of its n-th power agrees, modulo the (n + 1)-st power, with an R-linear combination of the monomials of degree n in the tⱼ.

theorem AlgHom.smul_sub_smul_mem_smul_top {R : Type u_3} {A : Type u_4} [CommRing R] [CommRing A] [Algebra R A] (χ : A →ₐ[R] R) {N : Type u_5} [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a : A) (x : N) : a • x - χ a • x ∈ RingHom.ker χ • ⊤

Modulo ker χ • N, the action of a on N agrees with that of its value χ a.