Documentation

Atlas.EllipticCurves.code.EndAlgClassification

A -algebra A equipped with an anti-involution invol together with a positive-definite reduced norm normMap : A → ℚ satisfying a * invol a = normMap a. This abstracts the structure of the Rosati involution on the endomorphism algebra of an abelian variety.

Instances

    The reduced trace tr(a) = N(a + 1) - N(a) - 1, induced by the reduced norm.

    Instances For
      inductive EndAlgClassification (A : Type u_1) [Ring A] [Algebra A] :

      Albert's classification of finite-dimensional positive-definite involution -algebras A: either A = ℚ (dimension 1), or A is an imaginary quadratic field (dimension 2 with a non-rational element squaring to a negative rational), or A is a definite quaternion algebra (dimension 4 with anticommuting generators squaring to negative rationals).

      Instances For
        theorem commuting_elements_in_subfield {A : Type u_1} [Ring A] [Algebra A] [PositiveDefiniteInvolutionAlgebra A] (α β : A) (hcomm : α * β = β * α) (hα_not_rat : ∀ (q : ), α (algebraMap A) q) :
        ∃ (r : ) (s : ), β = (algebraMap A) r + (algebraMap A) s * α

        In a positive-definite involution algebra, any element β that commutes with a non-rational element α lies in the -subalgebra generated by α: there exist r, s ∈ ℚ with β = r + s α. This is the crucial step that forces a 4-dimensional algebra to be a quaternion algebra.

        theorem pdi_make_anticommuting {A : Type u_1} [Ring A] [Algebra A] [PositiveDefiniteInvolutionAlgebra A] (α β₁ : A) (hinv_α : PositiveDefiniteInvolutionAlgebra.invol α = -α) (hinv_β₁ : PositiveDefiniteInvolutionAlgebra.invol β₁ = -β₁) (hα_sq : α * α = -(algebraMap A) (PositiveDefiniteInvolutionAlgebra.normMap α)) (hNα_pos : 0 < PositiveDefiniteInvolutionAlgebra.normMap α) (hias : ∀ (a : A), a + PositiveDefiniteInvolutionAlgebra.invol a = (algebraMap A) (PositiveDefiniteInvolutionAlgebra.traceMap a)) (hβ₁ni : ∀ (r s : ), β₁ (algebraMap A) r + (algebraMap A) s * α) :
        ∃ (β : A), PositiveDefiniteInvolutionAlgebra.invol β = -β α * β = -(β * α) (∀ (r s : ), β (algebraMap A) r + (algebraMap A) s * α) β 0

        Given a pure imaginary element α (anti-fixed by the involution) and a candidate β₁ not in the subfield ℚ[α], produce a pure imaginary element β anticommuting with α, by Gram-Schmidt style adjustment. This is a key step in constructing a quaternion basis.

        theorem quaternion_linIndep_four {A : Type u_1} [Ring A] [Algebra A] [PositiveDefiniteInvolutionAlgebra A] (α β : A) (hα_ne : α 0) (hα_not_rat : ∀ (q : ), α (algebraMap A) q) (hα_sq_val : α * α = (algebraMap A) (-PositiveDefiniteInvolutionAlgebra.normMap α)) (hanticomm : α * β = -(β * α)) (hβni : ∀ (r s : ), β (algebraMap A) r + (algebraMap A) s * α) (hNα_pos : 0 < PositiveDefiniteInvolutionAlgebra.normMap α) :

        In a positive-definite involution algebra A, the four elements {1, α, β, αβ} are -linearly independent whenever α is non-rational, anticommutes with β, β ∉ ℚ[α], and the norms behave as in a quaternion algebra.

        theorem endAlg_quaternion_finrank_four (A : Type u_1) [Ring A] [Algebra A] [PositiveDefiniteInvolutionAlgebra A] [Nontrivial A] (α β : A) (hα_ne : α 0) (hβ_ne : β 0) (hinv_α : PositiveDefiniteInvolutionAlgebra.invol α = -α) (hinv_β : PositiveDefiniteInvolutionAlgebra.invol β = -β) (hα_not_rat : ∀ (q : ), α (algebraMap A) q) (hα_sq_val : α * α = (algebraMap A) (-PositiveDefiniteInvolutionAlgebra.normMap α)) (hβ_sq_val : β * β = (algebraMap A) (-PositiveDefiniteInvolutionAlgebra.normMap β)) (hanticomm : α * β = -(β * α)) (hβni : ∀ (r s : ), β (algebraMap A) r + (algebraMap A) s * α) (hαβ_not_rat : ∀ (q : ), α * β (algebraMap A) q) (inv_add_self : ∀ (a : A), a + PositiveDefiniteInvolutionAlgebra.invol a = (algebraMap A) (PositiveDefiniteInvolutionAlgebra.traceMap a)) (inv_neg_of_ht : ∀ (a : A), PositiveDefiniteInvolutionAlgebra.invol (a - (algebraMap A) (PositiveDefiniteInvolutionAlgebra.traceMap a / 2)) = -(a - (algebraMap A) (PositiveDefiniteInvolutionAlgebra.traceMap a / 2))) :

        If A is a positive-definite involution algebra containing anticommuting pure imaginary elements α, β with the right norm properties, then A has -dimension exactly 4, with basis {1, α, β, αβ}.

        theorem endAlg_quaternion_case (A : Type u_1) [Ring A] [Algebra A] [PositiveDefiniteInvolutionAlgebra A] [Nontrivial A] (α : A) (hinv_α : PositiveDefiniteInvolutionAlgebra.invol α = -α) (hα_ne : α 0) (hα_not_rat : ∀ (q : ), α (algebraMap A) q) (hNα_pos : 0 < PositiveDefiniteInvolutionAlgebra.normMap α) (hα_sq_val : α * α = (algebraMap A) (-PositiveDefiniteInvolutionAlgebra.normMap α)) (inv_add_self : ∀ (a : A), a + PositiveDefiniteInvolutionAlgebra.invol a = (algebraMap A) (PositiveDefiniteInvolutionAlgebra.traceMap a)) (inv_neg_of_ht : ∀ (a : A), PositiveDefiniteInvolutionAlgebra.invol (a - (algebraMap A) (PositiveDefiniteInvolutionAlgebra.traceMap a / 2)) = -(a - (algebraMap A) (PositiveDefiniteInvolutionAlgebra.traceMap a / 2))) (hall_in_α : ¬∀ (a : A), ∃ (r : ) (s : ), a = (algebraMap A) r + (algebraMap A) s * α) :

        The quaternion case of Albert's classification: given a pure imaginary element α and an element not in ℚ[α], build a quaternion basis and conclude that A is a definite quaternion algebra.

        Albert's classification of endomorphism algebras: every nontrivial finite-dimensional positive-definite involution -algebra is either itself, an imaginary quadratic field, or a definite quaternion algebra.

        @[implicit_reducible]

        The endomorphism algebra End⁰(E) := End(E) ⊗_ℤ ℚ of an elliptic curve E carries a positive-definite involution algebra structure: the Rosati involution together with the reduced degree-norm.

        The Rosati involution on the endomorphism algebra of E, packaged as a function.

        Instances For

          The reduced norm End⁰(E) → ℚ (the rational extension of the degree map on End(E)).

          Instances For

            The reduced trace End⁰(E) → ℚ, defined as N(x + 1) - N(x) - 1.

            Instances For

              The Rosati involution is additive.

              The Rosati involution fixes the identity.

              The defining identity of the reduced norm: a * a^† = N(a) · 1 in the endomorphism algebra.

              The integer algebra map into the endomorphism ring is injective: the canonical map ℤ → End(E) has no kernel.

              The endomorphism algebra End⁰(E) is nontrivial: tensoring End(E) (a nontrivial ring with injective integer algebra map) with over remains nontrivial since is -flat.

              The endomorphism algebra End⁰(E) is a finite-dimensional -vector space.

              Specialization of Albert's classification to the endomorphism algebra of an elliptic curve: End⁰(E) is , an imaginary quadratic field, or a definite quaternion algebra.

              The endomorphism ring of an elliptic curve is torsion-free as a -module.

              The endomorphism ring of an elliptic curve is finitely generated as a -module.

              A finitely generated torsion-free -module is free; in particular, End(E) is -free.

              The -rank of End(E) is 1, 2, or 4, matching the three Albert cases.

              Combined freeness and rank statement for End(E): it is a free -module of rank 1, 2, or 4.