The group-theoretic filtration of a tame additive Néron fibre

This file isolates the exact algebra used after potentially good reduction has been established. It does not construct a Néron model. The narrow marked interface uses the actual quotient by a supplied identity subgroup and asks only that the marked component class have order at most four; a geometric consumer must prove that Tate--Kodaira statement for canonical nonsingular reduction. The downstream local modules already identify the formal kernel, classify the additive special fibre, and import its torsion-freeness theorem.

theorem MazurTorsion.EllipticCurve.map_eq_zero_of_addOrderOf_eq_of_coprime_card {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] [Finite H] (f : G →+ H) {P : G} {N : ℕ} (horder : addOrderOf P = N) (hcoprime : N.Coprime (Nat.card H)) : f P = 0

A homomorphism into a finite group kills a point of exact order N when N is coprime to the target cardinality.

def MazurTorsion.EllipticCurve.MarkedComponentOrderAtMost {G : Type u} [AddCommGroup G] (identitySubgroup : AddSubgroup G) (bound : ℕ) (P : G) : Prop

The marked-point part of the tame Kodaira component classification.

This predicate deliberately records the order of one point in the actual quotient by the specified identity subgroup. It is strictly narrower than finiteness or a cardinality bound for the whole component quotient. For a minimal elliptic equation with additive reduction in tame residue characteristic, the missing geometric input is that this predicate holds with bound four for the canonical nonsingular-reduction subgroup.

Equations

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

theorem MazurTorsion.EllipticCurve.markedComponentOrderAtMost_iff_exists_nsmul_mem {G : Type u} [AddCommGroup G] (identitySubgroup : AddSubgroup G) (bound : ℕ) (P : G) : MarkedComponentOrderAtMost identitySubgroup bound P ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ bound ∧ n • P ∈ identitySubgroup

The marked component-order predicate is equivalent to a completely pointwise certificate: some positive multiplier up to the bound sends the marked point into the identity subgroup. This is a useful target for a Tate-algorithm proof because it mentions neither finiteness nor the cardinality of the ambient quotient.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_of_markedComponentOrderAtMostFour {G : Type u} [AddCommGroup G] (identitySubgroup : AddSubgroup G) (P : G) (hP : MarkedComponentOrderAtMost identitySubgroup 4 P) : 12 • P ∈ identitySubgroup

A marked component class of finite order at most four is killed by the uniform tame exponent 12. This is the exact group-theoretic passage from the pointwise Kodaira assertion to the canonical identity subgroup; it does not construct or count the full component quotient.

theorem MazurTorsion.EllipticCurve.markedComponentOrderAtMost_of_quotient_card_le {G : Type u} [AddCommGroup G] (identitySubgroup : AddSubgroup G) [Finite (G ⧸ identitySubgroup)] (bound : ℕ) (hcard : Nat.card (G ⧸ identitySubgroup) ≤ bound) (P : G) : MarkedComponentOrderAtMost identitySubgroup bound P

A cardinality bound for the full component quotient implies the narrower marked-order certificate. This lemma is an explicit fallback for callers that already possess the stronger Néron component theorem; the marked-point consumers do not otherwise require such a bound.

theorem MazurTorsion.EllipticCurve.twelve_nsmul_mem_of_quotient_card_le_four {G : Type u} [AddCommGroup G] (identitySubgroup : AddSubgroup G) [Finite (G ⧸ identitySubgroup)] (hcard : Nat.card (G ⧸ identitySubgroup) ≤ 4) (P : G) : 12 • P ∈ identitySubgroup

The traditional full component-cardinality bound therefore gives the uniform marked exponent. Keeping this bridge separate makes the extra strength of that fallback visible in downstream theorem signatures.

theorem MazurTorsion.EllipticCurve.point_eq_zero_of_coprime_component_exponent {G : Type u} [AddCommGroup G] (identitySubgroup : AddSubgroup G) {ResidueAdditive : Type v} [AddCommGroup ResidueAdditive] [Finite ResidueAdditive] (identityReduction : ↥identitySubgroup →+ ResidueAdditive) (formalKernel : AddSubgroup ↥identitySubgroup) (identityReduction_ker : identityReduction.ker = formalKernel) (formalKernel_torsionFree : ∀ (Q : ↥formalKernel), IsOfFinAddOrder Q → Q = 0) {componentExponent N : ℕ} {P : G} (hN : N ≠ 0) (hcomponentCoprime : N.Coprime componentExponent) (hresidueCoprime : N.Coprime (Nat.card ResidueAdditive)) (hcomponentExponent : componentExponent • P ∈ identitySubgroup) (horder : addOrderOf P = N) : P = 0

A component-cardinality bound is stronger than the local torsion argument needs. It is enough to know that one integer coprime to the marked order sends the marked point into the identity subgroup. Reduction there, followed by the torsion-free formal kernel, then kills the point.

For a tame additive elliptic fibre the uniform integer used downstream is 12: it annihilates every group of order at most four, including the order-three component cases. Thus the geometric handoff may prove the narrower statement 12 • P ∈ E₀ without constructing or counting the full component quotient.

structure MazurTorsion.EllipticCurve.TameAdditiveFiltrationData (G : Type u) [AddCommGroup G] : Type (max u (v + 1))

The algebraic data in the filtration of local points of an elliptic curve with tame additive reduction. The component group is finite of size at most four; the identity component maps to the additive residue group; and the kernel of that map is the torsion-free formal kernel.

• Component : Type v
• componentAddCommGroup : AddCommGroup self.Component
• componentFinite : Finite self.Component
• ResidueAdditive : Type v
• residueAddCommGroup : AddCommGroup self.ResidueAdditive
• residueFinite : Finite self.ResidueAdditive
• component : G →+ self.Component
• identityReduction : ↥self.component.ker →+ self.ResidueAdditive
• formalKernel : AddSubgroup ↥self.component.ker
• identityReduction_ker : self.identityReduction.ker = self.formalKernel
• component_card_le_four : Nat.card self.Component ≤ 4
• formalKernel_torsionFree (Q : ↥self.formalKernel) : IsOfFinAddOrder Q → Q = 0

theorem MazurTorsion.EllipticCurve.TameAdditiveFiltrationData.point_eq_zero_of_coprime_card {G : Type u} [AddCommGroup G] (F : TameAdditiveFiltrationData G) {P : G} {N : ℕ} (hN : N ≠ 0) (hcomponent : N.Coprime (Nat.card F.Component)) (hresidue : N.Coprime (Nat.card F.ResidueAdditive)) (horder : addOrderOf P = N) : P = 0

If an order is coprime to both finite quotients in the tame additive filtration, a point of that exact order lies in the torsion-free formal kernel and hence vanishes.