Building a homomorphism from a ternary relation

Mathlib builds a MonoidHom out of a bare map from the two-variable identities f (x * y) = f x * f y (MonoidHom.mk') and f (x * y⁻¹) = f x * (f y)⁻¹ (MonoidHom.ofMapMulInv). Some maps are not naturally presented that way: they are defined by a symmetric ternary condition, and what one can prove about them directly is that they send triples with product 1 to triples with product 1. The motivating example is the descent map on an elliptic curve, whose defining property is that the classes of three collinear points multiply to 1 — collinearity being symmetric in the three points, whereas the group law is not.

Main results

• MonoidHom.ofMapMulMulEqOne: a map of groups with f 1 = 1 that sends triples with product 1 to triples with product 1 is a homomorphism, and MonoidHom.coe_ofMapMulMulEqOne says it is the original map. The additive versions are generated by to_additive.

Provenance

Adapted, with the author's proof, from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/Mathlib/Basic.lean.

def MonoidHom.ofMapMulMulEqOne {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf₁ : f 1 = 1) (hf : ∀ (a b c : G), a * b * c = 1 → f a * f b * f c = 1) : G →* H

A map f between groups with f 1 = 1 that sends triples with product 1 to triples with product 1 is a homomorphism. Useful when a map is naturally defined via a symmetric ternary relation, like collinearity on a cubic curve.

Equations

• MonoidHom.ofMapMulMulEqOne hf₁ hf = MonoidHom.ofMapMulInv f ⋯

def AddMonoidHom.ofMapAddAddEqZero {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf₁ : f 0 = 0) (hf : ∀ (a b c : G), a + b + c = 0 → f a + f b + f c = 0) : G →+ H

A map f between additive groups with f 0 = 0 that sends triples with sum 0 to triples with sum 0 is a homomorphism. Useful when a map is naturally defined via a symmetric ternary relation, like collinearity on a cubic curve.

Equations

• AddMonoidHom.ofMapAddAddEqZero hf₁ hf = AddMonoidHom.ofMapAddNeg f ⋯

@[simp]

theorem MonoidHom.coe_ofMapMulMulEqOne {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf₁ : f 1 = 1) (hf : ∀ (a b c : G), a * b * c = 1 → f a * f b * f c = 1) : ⇑(ofMapMulMulEqOne hf₁ hf) = f

The homomorphism built by MonoidHom.ofMapMulMulEqOne has the original map as its underlying function.

@[simp]

theorem AddMonoidHom.coe_ofMapAddAddEqZero {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf₁ : f 0 = 0) (hf : ∀ (a b c : G), a + b + c = 0 → f a + f b + f c = 0) : ⇑(ofMapAddAddEqZero hf₁ hf) = f

The homomorphism built by the additive constructor has the original map as its underlying function.