Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Isogeny.Separability

Separable and inseparable degrees of an isogeny #

TauCeti.Isogeny.degree is the dimension of W₁.FunctionField over the image of fieldPullback. That extension is finite, so it splits the degree into a separable and an inseparable part, and this file names those two parts and records that they multiply to the degree.

Main definitions #

Main results #

Design #

There is deliberately no Isogeny.IsSeparable predicate. Separability of φ is Algebra.IsSeparable φ.fieldPullback.fieldRange W₁.FunctionField — an existing Mathlib class applied to the extension degree already measures — and a wrapper around it would add a second name for one notion without adding a fact. The same holds for pure inseparability, which is IsPurelyInseparable on the same extension. What is not already sayable is the pair of numbers, so that is what this file adds.

Both definitions are unconditional: no separability hypothesis, so purely inseparable isogenies such as Frobenius are covered, matching Isogeny.finiteDimensional.

Multiplicativity under composition is separableDegree_comp and inseparableDegree_comp, matching degree_comp. Both run the tower F(W₃) ⊆ F(W₂) ⊆ F(W₁) against their own Mathlib tower law, through the transports off AlgHom.fieldRange beside finrank_fieldRange. The two are not quite symmetric: the separable law's algebraicity side condition is on the upper extension and the inseparable law's is on the lower one, so they call finiteDimensional_of_fieldRange on φ and on ψ respectively.

Provenance #

The degrees follow D. Angdinata's shared isogeny development in its function-field form; here they are written in the coordinate-ring form this repository's Isogeny uses.

The arithmetic content is Mathlib's — Field.finSepDegree_mul_finInsepDegree and the tower laws; this file transports it to isogenies along degree_def. No AINTLIB material is used: that source's isogeny development carries separability as a hypothesis rather than measuring it.

References #

source
noncomputable def TauCeti.Isogeny.separableDegree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
ℕ

The separable degree of an isogeny: the separable degree of W₁.FunctionField over the pulled-back copy of the target's function field.

Equations
Instances For
    source
    noncomputable def TauCeti.Isogeny.inseparableDegree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
    ℕ

    The inseparable degree of an isogeny, of the same extension.

    Equations
    Instances For
      source
      theorem TauCeti.Isogeny.separableDegree_def {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
      φ.separableDegree = Field.finSepDegree (↥φ.fieldPullback.fieldRange) W₁.FunctionField

      The defining formula for separableDegree. The definition's body is not exposed across the module boundary, so this is how downstream modules compute with it.

      source
      theorem TauCeti.Isogeny.inseparableDegree_def {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
      φ.inseparableDegree = Field.finInsepDegree (↥φ.fieldPullback.fieldRange) W₁.FunctionField

      The defining formula for inseparableDegree.

      source
      theorem TauCeti.Isogeny.separableDegree_eq_finSepDegree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) :
      φ.separableDegree = Field.finSepDegree W₂.FunctionField W₁.FunctionField

      The separable degree read off any algebra structure induced by the pullback, the separable analogue of degree_eq_finrank. Stated for an arbitrary structure whose map is fieldPullback, since registering one globally would be a diamond.

      source
      theorem TauCeti.Isogeny.inseparableDegree_eq_finInsepDegree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) :
      φ.inseparableDegree = Field.finInsepDegree W₂.FunctionField W₁.FunctionField

      The inseparable degree read off any algebra structure induced by the pullback.

      source
      theorem TauCeti.Isogeny.isSeparable_functionField {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] :
      Algebra.IsSeparable W₂.FunctionField W₁.FunctionField

      A separable isogeny induces a separable extension of function fields, for any algebra structure whose structure map is the pullback.

      Separability of φ is stated over φ.fieldPullback.fieldRange, but the theorems about the extension F(W₁)/F(W₂) — the fundamental identity, the different divisor, the Hurwitz genus formula — take it over W₂.FunctionField itself. This is the transport between the two, the separability counterpart of Isogeny.finiteDimensional_functionField.

      source
      @[simp]
      theorem TauCeti.Isogeny.separableDegree_mul_inseparableDegree {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
      φ.separableDegree * φ.inseparableDegree = φ.degree

      The degree factors as separable times inseparable. This is the field-theoretic factorisation transported to isogenies; it is what makes "the inseparable part is a Frobenius power" a statement about inseparableDegree.

      source
      theorem TauCeti.Isogeny.separableDegree_pos {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
      0 < φ.separableDegree

      Every isogeny has a strictly positive separable degree — in particular never zero, so this factor of separableDegree_mul_inseparableDegree can be cancelled against degree. It is frequently 1, which is nondegenerate: by separableDegree_eq_one_iff_isPurelyInseparable it characterises the purely inseparable case. Separability is characterised by inseparable degree 1.

      source
      theorem TauCeti.Isogeny.inseparableDegree_pos {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
      0 < φ.inseparableDegree

      Every isogeny has a strictly positive inseparable degree, likewise never zero, so either factor of separableDegree_mul_inseparableDegree may be cancelled against degree.

      source
      @[simp]
      theorem TauCeti.Isogeny.separableDegree_ne_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
      φ.separableDegree ≠ 0

      The separable degree of an isogeny is nonzero.

      source
      @[simp]
      theorem TauCeti.Isogeny.inseparableDegree_ne_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
      φ.inseparableDegree ≠ 0

      The inseparable degree of an isogeny is nonzero.

      source
      @[simp]
      theorem TauCeti.Isogeny.separableDegree_id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) :
      (id W).separableDegree = 1

      The identity isogeny has separable degree one.

      source
      @[simp]
      theorem TauCeti.Isogeny.inseparableDegree_id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) :
      (id W).inseparableDegree = 1

      The identity isogeny has inseparable degree one.

      source
      @[simp]
      theorem TauCeti.Isogeny.separableDegree_eq_degree_of_isSeparable {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] :
      φ.separableDegree = φ.degree

      A separable isogeny has separable degree equal to its degree.

      source
      @[simp]
      theorem TauCeti.Isogeny.inseparableDegree_eq_one_of_isSeparable {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] :
      φ.inseparableDegree = 1

      A separable isogeny has inseparable degree one.

      source
      @[simp]
      theorem TauCeti.Isogeny.separableDegree_eq_one_of_isPurelyInseparable {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsPurelyInseparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] :
      φ.separableDegree = 1

      A purely inseparable isogeny has separable degree one.

      source
      @[simp]
      theorem TauCeti.Isogeny.inseparableDegree_eq_degree_of_isPurelyInseparable {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [IsPurelyInseparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] :
      φ.inseparableDegree = φ.degree

      A purely inseparable isogeny carries its whole degree in the inseparable part.

      source
      theorem TauCeti.Isogeny.separableDegree_eq_one_iff_isPurelyInseparable {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
      φ.separableDegree = 1 ↔ IsPurelyInseparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField

      A separable degree of 1 characterises pure inseparability, not merely follows from it.

      The @[simp] lemmas above eliminate an assumed instance; this is the way back, for a consumer holding a computed degree and wanting the class. Both directions matter once [n] and Frobenius are in play, where the degree is what gets calculated.

      source
      theorem TauCeti.Isogeny.inseparableDegree_eq_one_iff_isSeparable {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) :
      φ.inseparableDegree = 1 ↔ Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField

      An inseparable degree of 1 characterises separability, the companion of separableDegree_eq_one_iff_isPurelyInseparable.

      source
      @[simp]
      theorem TauCeti.Isogeny.separableDegree_comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) :
      (ψ.comp φ).separableDegree = ψ.separableDegree * φ.separableDegree

      The separable degree is multiplicative under composition, by the tower formula for F(W₃) ⊆ F(W₂) ⊆ F(W₁), exactly as degree_comp.

      source
      @[simp]
      theorem TauCeti.Isogeny.inseparableDegree_comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) :
      (ψ.comp φ).inseparableDegree = ψ.inseparableDegree * φ.inseparableDegree

      The inseparable degree is multiplicative under composition, by the inseparable tower formula for F(W₃) ⊆ F(W₂) ⊆ F(W₁) — the inseparable counterpart of separableDegree_comp, and the second factor of degree_comp.

      source
      theorem TauCeti.Isogeny.isSeparable_comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥ψ.fieldPullback.fieldRange) W₂.FunctionField] [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] :
      Algebra.IsSeparable (↥(ψ.comp φ).fieldPullback.fieldRange) W₁.FunctionField

      A composite of separable isogenies is separable. This is a theorem, not a global instance; a consumer that needs the composite's separability as an instance activates it with attribute [local instance] isSeparable_comp.