FLT/GaloisRepresentation/HardlyRamified/Frey.lean

GitHub source file

3 declarations, 2 contain sorry, 0 declared as axioms

The Frey curve gives a hardly ramified representation

We prove that the ℓ-torsion of the Frey curve attached to a Frey package is a hardly ramified Galois representation, and that this representation is irreducible.

Imports (6)
Imported by 2 files
  1. instance (instance at line 35) line 35 source

    Source documentation

    We cannot hope to make a constructive decidable equality on AlgebraicClosure ℚ because it is defined in a completely nonconstructive way, so we add the classical instance.

    noncomputable instance : DecidableEq (AlgebraicClosure ℚ) := Classical.typeDecidableEq _
  2. theorem FreyCurve.torsion_isHardlyRamified sorry line 37 source

    depends on sorry what this means

    Statement uses: FreyPackage, GaloisRepresentation.IsHardlyRamified, FreyPackage.p, Fact.mk, Nat.Prime, FreyPackage.pp, FreyPackage.hp_odd, ZMod, WeierstrassCurve.nTorsion, AlgebraicClosure, Rat, WeierstrassCurve.map, FreyPackage.freyCurve, Algebra.algebraMap, Int, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, Submodule.torsionBy, sorryAx, Lean.Name and 12 more

    104 instances, coercions and auxiliary constants left out.

  3. theorem FreyCurve.torsion_not_isIrreducible sorry line 43 source

    depends on sorry what this means

    Statement uses: FreyPackage, Not, GaloisRep.IsIrreducible, Rat, WeierstrassCurve.nTorsion, AlgebraicClosure, WeierstrassCurve.map, FreyPackage.freyCurve, Algebra.algebraMap, FreyPackage.p, Int, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, Submodule.torsionBy, ZMod, Fact.mk, Nat.Prime, FreyPackage.pp, WeierstrassCurve.galoisRep, FreyPackage.hppos

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    49 instances, coercions and auxiliary constants left out.