Pre- and postcomposition with homomorphisms, as bijections on homomorphisms

For a homomorphism f : M →* N and a commutative monoid P, Mathlib's MonoidHom.compHom' f is precomposition with f, as a homomorphism (N →* P) →* M →* P. This file records that it is bijective as soon as f is: Hom(-, P) takes isomorphisms to isomorphisms. The bundled form of this fact is Mathlib's MulEquiv.monoidHomCongrLeft; the statement here is the one to use when the isomorphism is given as a homomorphism known to be bijective, and the precomposition map is the unbundled compHom'.

Dually, for f : N →* P between commutative monoids, MonoidHom.compHom f is postcomposition with f, as a homomorphism (M →* N) →* M →* P. It is bijective as soon as f is injective and its range contains every n-th root of unity of P, provided every element of M satisfies a ^ n = 1: a homomorphism out of M takes values in the n-th roots of unity, so Hom(M, -) sees such an f as an isomorphism. This is the form in which an injection of coefficient groups whose image is the n-torsion induces bijections on duals.

The same transport principle applies to a perfect biadditive pairing: bijective changes of both variables and of the target preserve bijectivity of its curried homomorphism.

Main results

• MonoidHom.compHom'_bijective, AddMonoidHom.compHom'_bijective: precomposition with a bijective homomorphism is bijective on homomorphisms into a commutative monoid.
• MonoidHom.compHom_bijective_of_forall_pow_eq_one, AddMonoidHom.compHom_bijective_of_forall_nsmul_eq_zero: postcomposition with an injective homomorphism onto the n-th roots of unity is bijective on homomorphisms out of a monoid killed by n.
• MonoidHom.compHom_bijective, AddMonoidHom.compHom_bijective: postcomposition with a bijective homomorphism is bijective on homomorphisms out of any monoid.
• AddMonoidHom.bijective_of_bijective_pairing: a perfect biadditive pairing remains perfect after bijective changes of variables and target.
• TauCeti.forall_eq_zero_and_exists_eq_of_bijective_of_addEquiv: a pairing that reads, through additive equivalences, as a bijective curried homomorphism separates the points of its second argument, and every homomorphism out of its first argument is pairing with some point.

theorem MonoidHom.compHom'_bijective {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [CommMonoid P] {f : M →* N} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑f.compHom'

Precomposition with a bijective homomorphism is bijective on homomorphisms into a commutative monoid: Hom(-, P) takes isomorphisms to isomorphisms. The inverse is precomposition with the inverse bijection.

theorem AddMonoidHom.compHom'_bijective {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] {f : M →+ N} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑f.compHom'

Precomposition with a bijective homomorphism is bijective on homomorphisms into a commutative additive monoid: Hom(-, P) takes isomorphisms to isomorphisms. The inverse is precomposition with the inverse bijection.

theorem AddMonoidHom.bijective_of_bijective_pairing {X : Type u_4} {X' : Type u_5} {Y : Type u_6} {Y' : Type u_7} {Z : Type u_8} {Z' : Type u_9} [AddMonoid X] [AddMonoid X'] [AddMonoid Y] [AddMonoid Y'] [AddCommMonoid Z] [AddCommMonoid Z'] (P : X →+ Y →+ Z) (P' : X' →+ Y' →+ Z') (eX : X' →+ X) (eY : Y' →+ Y) (eZ : Z →+ Z') (hX : Function.Bijective ⇑eX) (hY : Function.Bijective ⇑eY) (hZ : Function.Bijective ⇑eZ) (hP : Function.Bijective ⇑P) (hcomm : ∀ (x : X') (y : Y'), (P' x) y = eZ ((P (eX x)) (eY y))) : Function.Bijective ⇑P'

A biadditive pairing remains perfect after bijective changes of variables and target.

theorem TauCeti.forall_eq_zero_and_exists_eq_of_bijective_of_addEquiv {X : Type u_4} {Y : Type u_5} {X₀ : Type u_6} {Y₀ : Type u_7} {Z : Type u_8} [AddZeroClass X] [AddZeroClass Y] [AddZeroClass X₀] [AddZeroClass Y₀] [AddCommMonoid Z] (pair : X → Y → Z) (eX : X₀ ≃+ X) (eY : Y₀ ≃+ Y) (α : Y₀ →+ X₀ →+ Z) (hα : Function.Bijective ⇑α) (h : ∀ (x : X₀) (y : Y₀), pair (eX x) (eY y) = (α y) x) : (∀ (y : Y), (∀ (x : X), pair x y = 0) → y = 0) ∧ ∀ (ψ : X →+ Z), ∃ (y : Y), ∀ (x : X), pair x y = ψ x

A pairing pair : X → Y → Z that reads, through additive equivalences eX and eY, as a bijective curried homomorphism α : Y₀ → (X₀ →+ Z) separates the points of its second argument, and every homomorphism X →+ Z is pairing with some point of Y.

theorem MonoidHom.compHom_bijective_of_forall_pow_eq_one {M : Type u_4} {N : Type u_5} {P : Type u_6} [Monoid M] [CommMonoid N] [CommMonoid P] {f : N →* P} (hf : Function.Injective ⇑f) {n : ℕ} (hM : ∀ (a : M), a ^ n = 1) (hf' : ∀ (y : P), y ^ n = 1 → ∃ (x : N), f x = y) : Function.Bijective ⇑(compHom f)

Postcomposition with an injective homomorphism f : N →* P is bijective on homomorphisms out of a monoid M all of whose elements satisfy a ^ n = 1, provided the range of f contains every n-th root of unity of P: every homomorphism M →* P takes values in the n-th roots of unity, hence in the range of f, and so lifts uniquely through f.

theorem AddMonoidHom.compHom_bijective_of_forall_nsmul_eq_zero {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddMonoid M] [AddCommMonoid N] [AddCommMonoid P] {f : N →+ P} (hf : Function.Injective ⇑f) {n : ℕ} (hM : ∀ (a : M), n • a = 0) (hf' : ∀ (y : P), n • y = 0 → ∃ (x : N), f x = y) : Function.Bijective ⇑(compHom f)

Postcomposition with an injective homomorphism f : N →+ P is bijective on homomorphisms out of an additive monoid M all of whose elements satisfy n • a = 0, provided the range of f contains every element of P killed by n: every homomorphism M →+ P takes values in the n-torsion, hence in the range of f, and so lifts uniquely through f.

theorem MonoidHom.compHom_bijective {M : Type u_4} {N : Type u_5} {P : Type u_6} [Monoid M] [CommMonoid N] [CommMonoid P] {f : N →* P} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(compHom f)

Postcomposition with a bijective homomorphism f : N →* P is bijective on homomorphisms out of any monoid: Hom(M, -) takes isomorphisms to isomorphisms. This is the case n = 0 of MonoidHom.compHom_bijective_of_forall_pow_eq_one; the bundled form is Mathlib's MulEquiv.monoidHomCongrRightEquiv.

theorem AddMonoidHom.compHom_bijective {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddMonoid M] [AddCommMonoid N] [AddCommMonoid P] {f : N →+ P} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(compHom f)

Postcomposition with a bijective homomorphism f : N →+ P is bijective on homomorphisms out of any additive monoid: Hom(M, -) takes isomorphisms to isomorphisms. This is the case n = 0 of AddMonoidHom.compHom_bijective_of_forall_nsmul_eq_zero; the bundled form is Mathlib's AddEquiv.addMonoidHomCongrRightEquiv.