Forbidden additive-group embeddings

This file packages the recurring negative input in Mazur's torsion classification: a specified finite abelian group does not embed in the rational points of an elliptic curve. The definition is pure group theory, and the transport lemmas keep later arithmetic files independent of a particular presentation of either group.

def MazurTorsion.ForbidsEmbedding (A : Type u_1) (G : Type u_2) [AddCommGroup A] [AddCommGroup G] : Prop

There is no injective additive homomorphism from A to G.

Equations

• MazurTorsion.ForbidsEmbedding A G = ∀ (f : A →+ G), ¬Function.Injective ⇑f

theorem MazurTorsion.ForbidsEmbedding.of_injective_source {A : Type u_1} {B : Type u_2} {G : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup G] (h : ForbidsEmbedding A G) (f : A →+ B) (hf : Function.Injective ⇑f) : ForbidsEmbedding B G

If A embeds in B and A cannot embed in G, then B cannot embed in G.

theorem MazurTorsion.ForbidsEmbedding.of_injective_target {A : Type u_1} {G : Type u_3} {H : Type u_4} [AddCommGroup A] [AddCommGroup G] [AddCommGroup H] (h : ForbidsEmbedding A H) (f : G →+ H) (hf : Function.Injective ⇑f) : ForbidsEmbedding A G

If G embeds in H and A cannot embed in H, then A cannot embed in G.

theorem MazurTorsion.ForbidsEmbedding.addEquiv_source {A : Type u_1} {B : Type u_2} {G : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup G] (e : A ≃+ B) : ForbidsEmbedding A G ↔ ForbidsEmbedding B G

Transport the forbidden source along an additive equivalence.

theorem MazurTorsion.ForbidsEmbedding.addEquiv_target {A : Type u_1} {G : Type u_3} {H : Type u_4} [AddCommGroup A] [AddCommGroup G] [AddCommGroup H] (e : G ≃+ H) : ForbidsEmbedding A G ↔ ForbidsEmbedding A H

Transport the target along an additive equivalence.

theorem MazurTorsion.ForbidsEmbedding.subgroup_target {A : Type u_1} {G : Type u_3} [AddCommGroup A] [AddCommGroup G] (h : ForbidsEmbedding A G) (K : AddSubgroup G) : ForbidsEmbedding A ↥K

A forbidden embedding into a group is also forbidden into any additive subgroup.

theorem MazurTorsion.ForbidsEmbedding.not_nonempty_addEquiv {A : Type u_1} {G : Type u_3} [AddCommGroup A] [AddCommGroup G] (h : ForbidsEmbedding A G) : ¬Nonempty (A ≃+ G)

A forbidden embedding rules out an additive equivalence.