Canonical quotient data for tame additive reduction #
The abstract tame-additive filtration only needs two finite targets and a torsion-free formal kernel. For a Néron fibre, however, the component map is not arbitrary: its kernel is the identity subgroup and its target is the quotient by that subgroup. This file records that more geometric handoff and constructs the existing algebraic filtration from it.
The formal kernel is also not accepted with an unrelated torsion-freeness hypothesis. At the unramified primes five and eleven, the specializations below discharge torsion-freeness using the exact-pinned formal-group filtration theorem. What remains explicit is precisely the Néron geometry: the identity subgroup, its reduction map, identification of its kernel with the formal filtration, and the order-at-most-four component bound. Finiteness of the component quotient is derived from the exact-pin theorem that the formal filtration already has finite index.
The geometric data between local points and the group-theoretic tame-additive filtration.
identitySubgroup models the points reducing to the identity component. The component group is
not a supplied type: it is canonically G ⧸ identitySubgroup. Likewise, the formal kernel is a
fixed subgroup of G, required to lie in the identity subgroup and to be exactly the kernel of
identityReduction there.
- identitySubgroup : AddSubgroup G
- ResidueAdditive : Type u
- residueAddCommGroup : AddCommGroup self.ResidueAdditive
- residueFinite : Finite self.ResidueAdditive
- identityReduction_ker : self.identityReduction.ker = AddSubgroup.comap self.identitySubgroup.subtype formalKernel
- componentFinite : Finite (G ⧸ self.identitySubgroup)
Instances For
The actual component homomorphism to the quotient by the identity subgroup.
Equations
Instances For
The kernel of the canonical component map is additively equivalent to the specified identity subgroup. Both sides have the same underlying points; the equivalence only transports the checked kernel equality.
Equations
Instances For
Reduction on the kernel of the canonical component map.
Equations
Instances For
The formal subgroup inside the kernel of the canonical component map. It is definitionally
the kernel of identity-component reduction, while identityReduction_ker identifies its
underlying local points with the prescribed formal filtration.
Instances For
The prescribed formal subgroup is exactly the formal subgroup appearing inside the kernel
of the canonical component map. This equivalence uses
formalKernel_le_identity; it is not merely the intersection of two unrelated subgroups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Construct the algebraic tame-additive filtration from the canonical quotient data and a torsion-freeness theorem for the prescribed formal subgroup.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At five, the exact-pinned unramified formal-kernel theorem supplies the only torsion-freeness input needed by the canonical reduction data.
Equations
Instances For
The same canonical conversion at eleven, used by the squarefree-level order-35 route.
Equations
Instances For
The five-adic geometric handoff with the reduction target fixed to the actual additive residue field. Thus the target is no longer an arbitrary finite group of cardinality five. A Néron-model consumer must construct the identity subgroup and the displayed reduction homomorphism, and prove that its kernel is the exact-pinned formal filtration. Surjectivity onto the residue field is not required by the downstream torsion contradiction.
- identitySubgroup : AddSubgroup W.Point
- identityReduction : ↥self.identitySubgroup →+ IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atFive)
- identityReduction_ker : self.identityReduction.ker = AddSubgroup.comap self.identitySubgroup.subtype (WeierstrassCurve.Affine.filtration hW 0)
Instances For
The additive residue group in the five-adic geometric data has exactly five elements.
Forget only the fact that the reduction target has been fixed to the actual additive residue field. The identity subgroup, canonical component quotient, reduction map, and formal-kernel equality are retained literally.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Construct the final algebraic filtration. Formal-kernel torsion-freeness is discharged by
the checked unramified theorem, and residue cardinality is fixed by residue_natCard.
Equations
Instances For
The analogous eleven-adic handoff used by the order-35 formal-immersion route.
- identitySubgroup : AddSubgroup W.Point
- identityReduction : ↥self.identitySubgroup →+ IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)
- identityReduction_ker : self.identityReduction.ker = AddSubgroup.comap self.identitySubgroup.subtype (WeierstrassCurve.Affine.filtration hW 0)
Instances For
The additive residue group in the eleven-adic geometric data has exactly eleven elements.
Forget only the fixed eleven-adic reduction target, retaining the canonical component quotient, reduction map, and exact formal-kernel equality.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Construct the algebraic filtration using the checked exact-pinned theorem at eleven.