Documentation

RamanujanNagell.QuadraticIntegers.FieldIsomorphism

The field isomorphism K' ≃ₐ[ℚ] K #

We construct an explicit ℚ-algebra isomorphism between K' = QuadraticAlgebra ℚ (-7) 0 (ω' satisfies (ω')² = -7) K = QuadraticAlgebra ℚ (-2) 1 (ω satisfies ω² = -2 + ω)

The isomorphism sends ω' ↦ 2ω - 1 (in K), since: (2ω - 1)² = 4ω² - 4ω + 1 = 4(-2 + ω) - 4ω + 1 = -8 + 4ω - 4ω + 1 = -7 ✓

The inverse sends ω ↦ (ω' + 1)/2 (in K').

source
def toK :
QuadraticAlgebra ℚ (↑(-7)) 0 →ₐ[ℚ] Klocal✝

The ℚ-algebra map K' → K sending ω' ↦ 2ω - 1.

Equations
Instances For
    source
    def toK' :
    Klocal✝ →ₐ[ℚ] QuadraticAlgebra ℚ (↑(-7)) 0

    The ℚ-algebra map K → K' sending ω ↦ (ω' + 1)/2.

    Equations
    Instances For
      source
      def fieldIso :
      QuadraticAlgebra ℚ (↑(-7)) 0 ≃ₐ[ℚ] Klocal✝

      The field isomorphism K' ≃ₐ[ℚ] K.

      Equations
      Instances For
        source
        theorem fieldIso_omega :
        fieldIso QuadraticAlgebra.omega = 2 * QuadraticAlgebra.omega - 1

        The isomorphism sends ω' to 2ω - 1.

        source
        def OK_to_K :
        QuadraticAlgebra ℤ (-2) 1 →ₐ[ℤ] Klocal✝
        Equations
        Instances For
          source
          instance alg_int_K :
          Algebra (QuadraticAlgebra ℤ (-2) 1) Klocal✝
          Equations
          source
          instance hST :
          IsScalarTower ℤ (QuadraticAlgebra ℤ (-2) 1) Klocal✝
          source
          theorem quadraticAlgebra_adjoin_omega_eq_top (a b : ℤ) :
          Algebra.adjoin ℤ {QuadraticAlgebra.omega} = ⊤

          Every element of QuadraticAlgebra ℤ a b is generated by ω as a ℤ-algebra.

          source
          theorem isIntegralClosure_K [Algebra (QuadraticAlgebra ℤ (-2) 1) (QuadraticAlgebra ℚ (↑(-2)) 1)] [IsScalarTower ℤ (QuadraticAlgebra ℤ (-2) 1) (QuadraticAlgebra ℚ (↑(-2)) 1)] (h_omega : (algebraMap (QuadraticAlgebra ℤ (-2) 1) (QuadraticAlgebra ℚ (↑(-2)) 1)) QuadraticAlgebra.omega = QuadraticAlgebra.omega) :
          IsIntegralClosure (QuadraticAlgebra ℤ (-2) 1) ℤ (QuadraticAlgebra ℚ (↑(-2)) 1)

          QuadraticAlgebra ℤ (-2) 1 is an integral closure of ℤ in K, via the algebra map OK_to_K (sending ω ↦ ω). This is the transport of ring_of_integers_neg7 along fieldIso : K' ≃ₐ[ℚ] K.

          The explicit hypothesis h_omega pins down the algebra map algebraMap A K by requiring it sends ω to ω; at the call site (Helpers.lean), this is satisfied by OK_to_K.toAlgebra.