LeanPool.EcTateLean.Algebra.EllipticCurve.KodairaTypes

Imported Lean Pool material for LeanPool.EcTateLean.Algebra.EllipticCurve.KodairaTypes.

inductive Kodaira : Type

The Kodaira symbol classifying the reduction type of an elliptic curve at a place, including the extra symbols that arise over imperfect residue fields of characteristic 2 or 3.

• I : Nat → Kodaira
• II : Kodaira
• III : Kodaira
• IV : Kodaira
• Is : Nat → Kodaira
• IIs : Kodaira
• IIIs : Kodaira
• IVs : Kodaira
• Z1 : Kodaira
• Z2 : Kodaira
• X1 : Kodaira
• X2 : Kodaira
• Y1 : Kodaira
• Y2 : Kodaira
• Y3 : Kodaira
• K : Nat → Kodaira
• K' : Nat → Kodaira
• T : Nat → Kodaira

@[implicit_reducible]

instance instDecidableEqKodaira : DecidableEq Kodaira

Equations

• instDecidableEqKodaira = instDecidableEqKodaira.decEq

def instDecidableEqKodaira.decEq (x✝ x✝¹ : Kodaira) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instInhabitedKodaira : Inhabited Kodaira

Equations

• instInhabitedKodaira = { default := instInhabitedKodaira.default }

@[implicit_reducible]

instance instReprKodaira : Repr Kodaira

Equations

• One or more equations did not get rendered due to their size.

theorem eq_I_Nat (m n : Nat) : m = n ↔ Kodaira.I m = Kodaira.I n

theorem eq_Is_Nat (m n : Nat) : m = n ↔ Kodaira.Is m = Kodaira.Is n

inductive ReductionType : Type

The coarse reduction type of an elliptic curve at a place: good, split or non-split multiplicative, or additive.

• Good : ReductionType
• SplitMultiplicative : ReductionType
• NonSplitMultiplicative : ReductionType
• Additive : ReductionType

@[implicit_reducible]

instance instDecidableEqReductionType : DecidableEq ReductionType

Equations

• instDecidableEqReductionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprReductionType : Repr ReductionType

Equations

• instReprReductionType = { reprPrec := instReprReductionType.repr }

def instReprReductionType.repr : ReductionType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprReductionType.repr ReductionType.Good prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ReductionType.Good")).group prec✝
• instReprReductionType.repr ReductionType.Additive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ReductionType.Additive")).group prec✝

@[implicit_reducible]

instance instInhabitedReductionType : Inhabited ReductionType

Equations

• instInhabitedReductionType = { default := instInhabitedReductionType.default }

def ReductionType.toLmfdb : ReductionType → Int

The integer code that the LMFDB uses for a reduction type.

Equations

• ReductionType.Good.toLmfdb = panicWithPosWithDecl "LeanPool.EcTateLean.Algebra.EllipticCurve.KodairaTypes" "ReductionType.toLmfdb" 88 30 "unreachable code has been reached"
• ReductionType.SplitMultiplicative.toLmfdb = 1
• ReductionType.NonSplitMultiplicative.toLmfdb = -1
• ReductionType.Additive.toLmfdb = 0