Documentation

MazurTorsion.GroupTheory.IndependentCyclicGenerators

Embeddings from independent cyclic generators #

This file packages a small group-theoretic construction used after an explicit two-isogeny. A point P of exact order two and a point Q of exact order n generate an embedded ZMod 2 × ZMod n as soon as P does not lie in the cyclic subgroup generated by Q.

source
def MazurTorsion.IndependentCyclicGenerators.zmodHom {G : Type u_1} [AddCommGroup G] (n : ℕ) (P : G) (hP : n • P = 0) :
ZMod n →+ G

The homomorphism from ZMod n which sends 1 to P.

Equations
Instances For
    source
    @[simp]
    theorem MazurTorsion.IndependentCyclicGenerators.zmodHom_intCast {G : Type u_1} [AddCommGroup G] (n : ℕ) (P : G) (hP : n • P = 0) (z : ℤ) :
    (zmodHom n P hP) ↑z = z • P
    source
    @[simp]
    theorem MazurTorsion.IndependentCyclicGenerators.zmodHom_one {G : Type u_1} [AddCommGroup G] (n : ℕ) (P : G) (hP : n • P = 0) :
    (zmodHom n P hP) 1 = P
    source
    theorem MazurTorsion.IndependentCyclicGenerators.zmodHom_injective {G : Type u_1} [AddCommGroup G] (n : ℕ) (P : G) (hP : n • P = 0) (horder : addOrderOf P = n) :
    Function.Injective ⇑(zmodHom n P hP)

    Exact order makes the cyclic-generator homomorphism injective.

    source
    def MazurTorsion.IndependentCyclicGenerators.productHom {G : Type u_1} [AddCommGroup G] (P Q : G) (hP : 2 • P = 0) (n : ℕ) (hQ : n • Q = 0) :
    ZMod 2 × ZMod n →+ G

    The sum of the two cyclic-generator maps.

    Equations
    Instances For
      source
      @[simp]
      theorem MazurTorsion.IndependentCyclicGenerators.productHom_apply {G : Type u_1} [AddCommGroup G] (P Q : G) (hP : 2 • P = 0) (n : ℕ) (hQ : n • Q = 0) (z : ZMod 2 × ZMod n) :
      (productHom P Q hP n hQ) z = (zmodHom 2 P hP) z.1 + (zmodHom n Q hQ) z.2
      source
      theorem MazurTorsion.IndependentCyclicGenerators.productHom_injective {G : Type u_1} [AddCommGroup G] (P Q : G) (hPorder : addOrderOf P = 2) (n : ℕ) (hQorder : addOrderOf Q = n) (hindependent : P ∉ AddSubgroup.zmultiples Q) :
      Function.Injective ⇑(productHom P Q ⋯ n ⋯)

      The product map is injective when the order-two generator is not in the cyclic subgroup generated by the other generator.

      source
      theorem MazurTorsion.IndependentCyclicGenerators.exists_embedding {G : Type u_1} [AddCommGroup G] (P Q : G) (hPorder : addOrderOf P = 2) (n : ℕ) (hQorder : addOrderOf Q = n) (hindependent : P ∉ AddSubgroup.zmultiples Q) :
      ∃ (f : ZMod 2 × ZMod n →+ G), Function.Injective ⇑f

      Existence form suited to a ForbidsEmbedding contradiction.

      source
      theorem MazurTorsion.IndependentCyclicGenerators.orderTwo_not_mem_zmultiples {G : Type u_1} [AddCommGroup G] (P Q : G) (n : ℕ) (hPorder : addOrderOf P = 2) (hQorder : addOrderOf Q = 2 * n) (hhalf : P ≠ n • Q) :
      P ∉ AddSubgroup.zmultiples Q

      In a cyclic group of exact order 2n, the sole nonzero point killed by two is the n-multiple of a generator. Consequently, any other point of exact order two is outside that cyclic subgroup.