Documentation

TauCeti.Algebra.Module.ZMod.Extend

Extending additive homomorphisms between groups killed by n #

Two mechanisms make Hom(-, W) exact on additive commutative groups killed by a natural number n, and both are recorded here as extension statements along an injective homomorphism f : A ā†’+ B with B killed by n.

For n = p prime, B is an š”½_p-vector space through AddCommGroup.zmodModule, and every additive homomorphism between two such groups is š”½_p-linear. Since an injective linear map of vector spaces has a linear left inverse, an injective additive homomorphism into a group killed by p has an additive left inverse, and so an additive homomorphism out of its source, with values in an arbitrary additive monoid N, extends along it. In other words, Hom(-, N) is exact on the additive groups killed by p for every N. Primality is essential for this: with p = 4, the identity of 2ā„¤/4ā„¤ ā‰… ā„¤/2ā„¤ does not extend along the inclusion 2ā„¤/4ā„¤ āŠ† ā„¤/4ā„¤ to a homomorphism ā„¤/4ā„¤ ā†’ ā„¤/2ā„¤, since every such homomorphism kills 2ā„¤/4ā„¤.

For arbitrary n the extension property holds for the targets W that are injective ā„¤/nā„¤-modules, in the form of Baer's criterion Module.Baer (ZMod n) W: an additive homomorphism A ā†’+ W between ā„¤/nā„¤-modules is linear, and Module.Baer.extension_property extends it along f. The case n = 0 is the extension property of a divisible group, and for n ā‰  0 the target W = ā„¤/nā„¤ is covered by Module.Baer.zmod_self.

Both extension statements make Hom(-, W) exact on the groups killed by n (Function.Exact.compHom' and Function.Exact.compHom'_of_baer, through the common Function.Exact.compHom'_of_forall_exists_comp_eq). These are the algebraic inputs to the duality statements for the finite š”½_p[G]-modules and the finite ā„¤/pā±[G]-modules of a profinite group.

Main results #

source
theorem AddMonoidHom.exists_comp_eq_of_injective {p : ā„•} [Fact (Nat.Prime p)] {A : Type u_1} {B : Type u_2} {N : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommMonoid N] (hB : āˆ€ (b : B), p ā€¢ b = 0) {f : A ā†’+ B} (hf : Function.Injective ā‡‘f) (Ļ† : A ā†’+ N) :
āˆƒ (Ļˆ : B ā†’+ N), Ļˆ.comp f = Ļ†

Extension along an injection into a group killed by a prime. If p is prime and B is killed by p, every additive homomorphism Ļ† : A ā†’+ N extends along an injective additive homomorphism f : A ā†’+ B to a homomorphism Ļˆ : B ā†’+ N with Ļˆ āˆ˜ f = Ļ†. No hypothesis is needed on N: the extension is Ļ† composed with an additive left inverse of f.

source
theorem AddMonoidHom.exists_comp_eq_of_injective_of_baer {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] {n : ā„•} {W : Type u_4} [AddCommGroup W] [Module (ZMod n) W] (hW : Module.Baer (ZMod n) W) (hB : āˆ€ (b : B), n ā€¢ b = 0) {f : A ā†’+ B} (hf : Function.Injective ā‡‘f) (Ļ† : A ā†’+ W) :
āˆƒ (Ļˆ : B ā†’+ W), Ļˆ.comp f = Ļ†

Extension along an injection into a group killed by n, into a Baer target. If B is killed by n and W satisfies Baer's criterion over ā„¤/nā„¤, then every additive homomorphism Ļ† : A ā†’+ W extends along an injective additive homomorphism f : A ā†’+ B to a homomorphism Ļˆ : B ā†’+ W with Ļˆ āˆ˜ f = Ļ†. The groups A and B are ā„¤/nā„¤-modules, every additive homomorphism between ā„¤/nā„¤-modules is linear, and Module.Baer.extension_property extends the linear map Ļ† along f. At n = 0 this is the extension property of a divisible group.

source
theorem Function.Exact.compHom'_of_forall_exists_comp_eq {X : Type u_4} {Y : Type u_5} {Z : Type u_6} {W : Type u_7} [AddCommGroup X] [AddCommGroup Y] [AddCommGroup Z] [AddCommMonoid W] {f : X ā†’+ Y} {g : Y ā†’+ Z} (h : Exact ā‡‘f ā‡‘g) (hext : āˆ€ (Ļ† : Y ā§ø g.ker ā†’+ W), āˆƒ (Ļˆ : Z ā†’+ W), Ļˆ.comp (QuotientAddGroup.kerLift g) = Ļ†) :
Exact ā‡‘g.compHom' ā‡‘f.compHom'

Exactness of Hom(-, W) from an extension property. If X ā†’ Y ā†’ Z is an exact pair of additive homomorphisms and every additive homomorphism Y ā§ø ker g ā†’+ W is the restriction along the embedding Y ā§ø ker g ā†’ Z induced by g of a homomorphism Z ā†’+ W, then the pair Hom(Z, W) ā†’ Hom(Y, W) ā†’ Hom(X, W) obtained by precomposition is exact. A homomorphism on Y killing the range of f, which is the kernel of g, descends to Y ā§ø ker g, and extends from there along the embedding of Y ā§ø ker g into Z.

source
theorem Function.Exact.compHom' {p : ā„•} [Fact (Nat.Prime p)] {X : Type u_4} {Y : Type u_5} {Z : Type u_6} {W : Type u_7} [AddCommGroup X] [AddCommGroup Y] [AddCommGroup Z] [AddCommMonoid W] {f : X ā†’+ Y} {g : Y ā†’+ Z} (h : Exact ā‡‘f ā‡‘g) (hZ : āˆ€ (z : Z), p ā€¢ z = 0) :
Exact ā‡‘g.compHom' ā‡‘f.compHom'

Hom(-, W) is exact on groups killed by a prime. If X ā†’ Y ā†’ Z is an exact pair of additive homomorphisms with Z killed by p, then for every additive commutative monoid W the pair Hom(Z, W) ā†’ Hom(Y, W) ā†’ Hom(X, W) obtained by precomposition is exact: every homomorphism out of Y ā§ø ker g extends along its embedding into Z, by AddMonoidHom.exists_comp_eq_of_injective.

source
theorem Function.Exact.compHom'_of_baer {n : ā„•} {X : Type u_4} {Y : Type u_5} {Z : Type u_6} {W : Type u_7} [AddCommGroup X] [AddCommGroup Y] [AddCommGroup Z] [AddCommGroup W] [Module (ZMod n) W] (hW : Module.Baer (ZMod n) W) {f : X ā†’+ Y} {g : Y ā†’+ Z} (h : Exact ā‡‘f ā‡‘g) (hZ : āˆ€ (z : Z), n ā€¢ z = 0) :
Exact ā‡‘g.compHom' ā‡‘f.compHom'

Hom(-, W) is exact on groups killed by n, for a Baer target. If X ā†’ Y ā†’ Z is an exact pair of additive homomorphisms with Z killed by n, and W satisfies Baer's criterion over ā„¤/nā„¤, then the pair Hom(Z, W) ā†’ Hom(Y, W) ā†’ Hom(X, W) obtained by precomposition is exact: every homomorphism out of Y ā§ø ker g extends along its embedding into Z, by AddMonoidHom.exists_comp_eq_of_injective_of_baer.