Frobenius and composition of isogenies

Over a finite field, the Frobenius commutes with every isogeny because every function-field homomorphism commutes with raising to the cardinality of the ground field. Its action by composition on the additive group of morphisms is additive. This is the Frobenius-specific distributivity needed to calculate in the subgroup generated by the identity and Frobenius. Composition with Frobenius is also injective on morphisms.

Main results

• TauCeti.Isogeny.frobeniusIsogeny_comp: Frobenius commutes with an isogeny.
• TauCeti.Isogeny.Hom.frobenius_comp: Frobenius is central in the endomorphism carrier.
• TauCeti.Isogeny.Hom.frobenius_comp_add: composition by Frobenius preserves addition.
• TauCeti.Isogeny.Hom.frobenius_comp_injective and TauCeti.Isogeny.Hom.frobenius_comp_inj: composition with Frobenius cancels.

References

• J. Silverman, The Arithmetic of Elliptic Curves, V.1–2.

theorem TauCeti.Isogeny.frobeniusIsogeny_comp {F : Type u_1} [Field F] [Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : (frobeniusIsogeny W₂).comp φ = φ.comp (frobeniusIsogeny W₁)

Frobenius commutes with an isogeny defined over the finite ground field.

theorem TauCeti.Isogeny.Hom.frobenius_comp {F : Type u_1} [Field F] [Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} (f : Hom W₁ W₂) : (ofIsogeny (frobeniusIsogeny W₂)).comp f = f.comp (ofIsogeny (frobeniusIsogeny W₁))

Frobenius commutes with every morphism, including the zero morphism.

@[simp]

theorem TauCeti.Isogeny.Hom.frobenius_comp_add {F : Type u_1} [Field F] [Finite F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (f g : Hom W₁ W₂) : (ofIsogeny (frobeniusIsogeny W₂)).comp (f + g) = (ofIsogeny (frobeniusIsogeny W₂)).comp f + (ofIsogeny (frobeniusIsogeny W₂)).comp g

Frobenius preserves sums of morphisms under composition.

theorem TauCeti.Isogeny.Hom.frobenius_comp_injective {F : Type u_1} [Field F] [Finite F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] {W₁ : WeierstrassCurve.Affine F} : Function.Injective fun (f : Hom W₁ W) => (ofIsogeny (frobeniusIsogeny W)).comp f

Composition with Frobenius cancels: f ↦ π ∘ f is injective on morphisms.

@[simp]

theorem TauCeti.Isogeny.Hom.frobenius_comp_inj {F : Type u_1} [Field F] [Finite F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] {W₁ : WeierstrassCurve.Affine F} {f g : Hom W₁ W} : (ofIsogeny (frobeniusIsogeny W)).comp f = (ofIsogeny (frobeniusIsogeny W)).comp g ↔ f = g

Two morphisms agree exactly when they agree after composition with Frobenius.