The class-group map induced by an isogeny

For an isogeny φ : Isogeny W₁ W₂, extending an ideal of W₁.CoordinateRing into the intermediate ring and taking the relative norm down to W₂.CoordinateRing gives a homomorphism of class groups.

Main definitions

• TauCeti.Isogeny.pushClassMonoidHom: the multiplicative form, ClassGroup W₁.CoordinateRing →* ClassGroup W₂.CoordinateRing.
• TauCeti.Isogeny.pushClass: the same map written additively, which is the form the point group consumes.

Main results

• TauCeti.Isogeny.pushClassMonoidHom_apply: the map on a class is the relative norm of that class extended into the intermediate ring.
• TauCeti.Isogeny.pushClassMonoidHom_mk0: when the source coordinate ring is normal, the map on the class of an integral ideal is the relative norm of its extension.
• TauCeti.Isogeny.pushClassMonoidHom_mk0_eq_one_of_map_eq_top: an integral ideal extending to the unit ideal of the intermediate ring has trivial image.
• TauCeti.Isogeny.pushClass_apply: the additive form is the multiplicative one transported along Additive.
• TauCeti.Isogeny.pushClassMonoidHom_id and TauCeti.Isogeny.pushClass_id: the identity isogeny induces the identity on class groups.

Design

Every algebra structure is built here, not accepted. Isogeny.intermediateRing is a Subring W₁.FunctionField carrying no Algebra instance over either coordinate ring — IntermediateRing/Basic.lean records that an instance would reintroduce a diamond — so the two structures have to come from somewhere. Taking them as arguments would leave the exported map a family indexed by the caller's choice: the hypotheses do not force them to be toIntermediateRing and pullbackToIntermediateRing, since injectivity, finiteness and Dedekindness are all stable under precomposing with an F-automorphism of the coordinate ring. So nothing in the signature would pin the map to the one φ induces, nor even make (Isogeny.id W).pushClass the identity. The definitions below therefore build both structures internally from the corestricted embeddings, which is what makes them the maps induced by φ, and what a functoriality statement and toPointHom need.

The same applies to the ambient structures the intermediate-ring suppliers ask for, Algebra W₂.CoordinateRing W₁.FunctionField and Algebra W₂.FunctionField W₁.FunctionField: they are φ.pullback and φ.fieldPullback read as algebra structures, and their tower is Isogeny.fieldPullback_algebraMap. Taking them as arguments would need a hypothesis pinning the first to the pullback for Isogeny.isScalarTower_intermediateRing to consume; building them makes that hypothesis rfl and removes it from the signature.

Every other hypothesis is discharged internally, from suppliers that live with the object they describe, in the one-property-per-file IntermediateRing/ series:

• the target coordinate ring's Dedekind property — WeierstrassCurve.Affine.isDedekindDomain_coordinateRing_of_isIntegrallyClosed, which is why target normality is what the maps ask for and the Dedekind property is not assumed;
• IsDedekindDomain φ.intermediateRing — Isogeny.isDedekindDomain_intermediateRing, which asks nothing of the function-field extension and so covers inseparable isogenies;
• Module.Finite W₂.CoordinateRing φ.intermediateRing — Isogeny.moduleFinite_intermediateRing, whose finite-normalization proof asks neither separability nor normality of the source;
• both Module.IsTorsionFree instances — Mathlib's Module.isTorsionFree_iff_algebraMap_injective applied to Isogeny.toIntermediateRing_injective and Isogeny.pullbackToIntermediateRing_injective. These are what make ClassGroup.extendedRelNormHom applicable at all: its variable block requires them.

What remains in the maps' signature is normality of the target coordinate ring. Source normality is needed only by pushClassMonoidHom_mk0, because Mathlib's computation rule for ClassGroup.mk0 assumes its source is Dedekind.

ClassGroup.extendedRelNormHom orders its rings A M R — source, middle, target — so the instantiation is A := W₁.CoordinateRing, M := φ.intermediateRing, R := W₂.CoordinateRing.

Provenance

⚠ mathlib-track. Adapted from D. Angdinata's shared isogeny development, Isogeny.lean, by David Kurniadi Angdinata, declarations pushClassMonoidHom and pushClass, which builds pushClass by ideal extension and relative norm (ClassGroup.extendedRelNormHom) on the way to toPointHom.

Two adaptations are forced by how this repository states the surrounding API:

• the source writes ClassGroup.extendedRelNormHom W₂.CoordinateRing W₁.CoordinateRing f.IntermediateRing, ordering the rings target-source-middle; TauCeti.ClassGroup's own extendedRelNormHom orders them source-middle-target, so the arguments are permuted here;
• the source obtains its algebra structures from a letI := f.pullback.coordinateRingAlgebra inside each proof; intermediateRing here carries no such instance by design, so the same is done from the corestricted embeddings, but inside the definition rather than inside a proof — which is what lets the exported map be canonical.

noncomputable def TauCeti.Isogeny.pushClassMonoidHom {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsIntegrallyClosed W₂.CoordinateRing] : ClassGroup W₁.CoordinateRing →* ClassGroup W₂.CoordinateRing

The class-group map induced by an isogeny, multiplicatively: extend a class of W₁.CoordinateRing into the intermediate ring, then norm it down to W₂.CoordinateRing.

The two coordinate rings carry no map between them; the intermediate ring is what connects them, receiving W₁.CoordinateRing by inclusion and lying module-finite over W₂.CoordinateRing.

Equations

• φ.pushClassMonoidHom = ClassGroup.extendedRelNormHom W₁.CoordinateRing (↥φ.intermediateRing) W₂.CoordinateRing

@[simp]

theorem TauCeti.Isogeny.pushClassMonoidHom_mk0 {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsIntegrallyClosed W₂.CoordinateRing] [IsIntegrallyClosed W₁.CoordinateRing] (I : ↥(nonZeroDivisors (Ideal W₁.CoordinateRing))) : φ.pushClassMonoidHom (ClassGroup.mk0 I) = ClassGroup.mk0 ((Ideal.relNorm0 W₂.CoordinateRing) (ClassGroup.extendedIdeal W₁.CoordinateRing (↥φ.intermediateRing) I))

The induced map on an integral ideal's class is the relative norm, down to W₂.CoordinateRing, of the ideal extended into the intermediate ring.

theorem TauCeti.Isogeny.pushClassMonoidHom_mk0_eq_one_of_map_eq_top {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsIntegrallyClosed W₂.CoordinateRing] [IsIntegrallyClosed W₁.CoordinateRing] (I : ↥(nonZeroDivisors (Ideal W₁.CoordinateRing))) (hI : Ideal.map φ.toIntermediateRing ↑I = ⊤) : φ.pushClassMonoidHom (ClassGroup.mk0 I) = 1

An ideal extending to the unit ideal of the intermediate ring has trivial class under the induced map: the relative norm of the unit ideal is the unit ideal.

theorem TauCeti.Isogeny.pushClassMonoidHom_apply {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsIntegrallyClosed W₂.CoordinateRing] (c : ClassGroup W₁.CoordinateRing) : φ.pushClassMonoidHom c = ClassGroup.relNorm ((ClassGroup.extendedHom W₁.CoordinateRing ↥φ.intermediateRing) c)

The induced map on a class is the relative norm, down to W₂.CoordinateRing, of that class extended into the intermediate ring. This is ClassGroup.extendedRelNormHom_apply for the structures the definition builds, so that consumers never have to unfold pushClassMonoidHom itself.

noncomputable def TauCeti.Isogeny.pushClass {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsIntegrallyClosed W₂.CoordinateRing] : Additive (ClassGroup W₁.CoordinateRing) →+ Additive (ClassGroup W₂.CoordinateRing)

The additive form of Isogeny.pushClassMonoidHom. The point group is described additively by its class group, so this is the shape the induced map on points is built from.

Equations

• φ.pushClass = MonoidHom.toAdditive φ.pushClassMonoidHom

@[simp]

theorem TauCeti.Isogeny.pushClass_apply {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsIntegrallyClosed W₂.CoordinateRing] (x : Additive (ClassGroup W₁.CoordinateRing)) : φ.pushClass x = Additive.ofMul (φ.pushClassMonoidHom (Additive.toMul x))

The additive form is the multiplicative one, transported along Additive.

@[simp]

theorem TauCeti.Isogeny.pushClassMonoidHom_id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [IsIntegrallyClosed W.CoordinateRing] : (id W).pushClassMonoidHom = MonoidHom.id (ClassGroup W.CoordinateRing)

The identity isogeny induces the identity on class groups. Its intermediate ring is the coordinate ring itself, so extending a class into it and norming it back down leaves the class unchanged.

@[simp]

theorem TauCeti.Isogeny.pushClass_id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [IsIntegrallyClosed W.CoordinateRing] : (id W).pushClass = AddMonoidHom.id (Additive (ClassGroup W.CoordinateRing))

The identity isogeny induces the identity, additively.