Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionTower

Towers of exact constant extensions #

Let C be the exact constant field of N, let M be an intermediate field in a tower C ⊆ M ⊆ N, and let S / C be finite Galois. Tensoring the inclusion M → N with the identity of S gives

S ⊗[C] M → S ⊗[C] N.

This file packages that map as the algebra structure needed by the constant-extension place and Frobenius APIs. It proves that the extended top is finite Galois over the extended intermediate field, with the same degree and hence the same Galois-group cardinality as N / M.

source
theorem BGS.HasseWeil.algebraicClosure_eq_bot_of_tower (C : Type u_1) (M : Type u_2) (N : Type u_3) [Field C] [Field M] [Field N] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] (hExactN : algebraicClosure C N = ⊥) :
algebraicClosure C M = ⊥

Exact constants descend from a field to every intermediate field in a compatible scalar tower.

source
noncomputable def BGS.HasseWeil.exactConstantExtensionTowerAlgHom (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] [Algebra C S] :
ExactConstantExtension C M S →ₐ[C] ExactConstantExtension C N S

Tensor the inclusion M → N with the identity on the enlarged constant field.

Equations
Instances For
    source
    @[simp]
    theorem BGS.HasseWeil.exactConstantExtensionTowerAlgHom_tmul (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] [Algebra C S] (s : S) (m : M) :
    (exactConstantExtensionTowerAlgHom C M N S) (s ⊗ₜ[C] m) = s ⊗ₜ[C] (algebraMap M N) m
    source
    @[reducible]
    noncomputable def BGS.HasseWeil.exactConstantExtensionTowerAlgebra (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] [Algebra C S] :
    Algebra (ExactConstantExtension C M S) (ExactConstantExtension C N S)

    The algebra structure on the extended top induced by the tensor map.

    Equations
    Instances For
      source
      theorem BGS.HasseWeil.exactConstantExtensionTower_leftScalarTower (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] [Algebra C S] :
      IsScalarTower S (ExactConstantExtension C M S) (ExactConstantExtension C N S)

      The tensor map preserves the enlarged constants on the left factor.

      source
      theorem BGS.HasseWeil.exactConstantExtensionTower_rightScalarTower (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExactN : algebraicClosure C N = ⊥) :
      have hExactM := ⋯; IsScalarTower M (ExactConstantExtension C M S) (ExactConstantExtension C N S)

      The tensor map also preserves the original right factor M.

      source
      theorem BGS.HasseWeil.exactConstantExtensionTower_finiteDimensional (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [FiniteDimensional M N] (hExactN : algebraicClosure C N = ⊥) :
      have hExactM := ⋯; FiniteDimensional (ExactConstantExtension C M S) (ExactConstantExtension C N S)

      The extended top is finite-dimensional over the extended intermediate field.

      source
      theorem BGS.HasseWeil.exactConstantExtensionTower_isGalois (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [FiniteDimensional M N] [IsGalois M N] (hExactN : algebraicClosure C N = ⊥) :
      have hExactM := ⋯; IsGalois (ExactConstantExtension C M S) (ExactConstantExtension C N S)

      Base change by finite constants preserves the Galois extension.

      source
      theorem BGS.HasseWeil.exactConstantExtensionTower_finrank (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [FiniteDimensional M N] (hExactN : algebraicClosure C N = ⊥) :
      have hExactM := ⋯; Module.finrank (ExactConstantExtension C M S) (ExactConstantExtension C N S) = Module.finrank M N

      Finite constant base change preserves the relative extension degree.

      source
      theorem BGS.HasseWeil.exactConstantExtensionTower_card_aut_eq (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra C M] [Algebra C N] [Algebra M N] [IsScalarTower C M N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [FiniteDimensional M N] [IsGalois M N] (hExactN : algebraicClosure C N = ⊥) :
      have hExactM := ⋯; Nat.card (ExactConstantExtension C N S ≃ₐ[ExactConstantExtension C M S] ExactConstantExtension C N S) = Nat.card Gal(N/M)

      Consequently the Galois group has the same finite cardinality after constant base change.

      source
      @[reducible]
      noncomputable def BGS.HasseWeil.exactConstantExtensionTowerCanonicalConstantAlgebra (C : Type u_5) (T : Type u_6) [Field C] [Field T] [Algebra (RatFunc C) T] :
      Algebra C T

      The constant algebra obtained by restricting a rational-function-field algebra along C → C(X). Naming this definition makes the canonical constant structures in the source and target definitionally transparent.

      Equations
      Instances For
        source
        theorem BGS.HasseWeil.exactConstantExtensionTowerCanonicalConstantScalarTower (C : Type u_1) (M : Type u_2) (N : Type u_3) [Field C] [Field M] [Field N] [Algebra (RatFunc C) M] [Algebra (RatFunc C) N] [Algebra M N] [IsScalarTower (RatFunc C) M N] :
        IsScalarTower C M N

        Restricting a compatible C(X)-tower along C → C(X) gives the canonical constant scalar tower used by exact constant extensions.

        source
        noncomputable def BGS.HasseWeil.exactConstantExtensionTowerRatFuncAlgHom (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra (RatFunc C) M] [Algebra (RatFunc C) N] [Algebra M N] [IsScalarTower (RatFunc C) M N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExactN : algebraicClosure C N = ⊥) :
        have hExactM := ⋯; let E_M := ExactConstantExtension C M S; let E_N := ExactConstantExtension C N S; E_M →ₐ[RatFunc S] E_N

        The tensor map between two exact constant extensions is linear over the enlarged rational-function field S(X) for the canonical structures on both extensions.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[reducible]
          noncomputable def BGS.HasseWeil.exactConstantExtensionTowerRatFuncAlgebra (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra (RatFunc C) M] [Algebra (RatFunc C) N] [Algebra M N] [IsScalarTower (RatFunc C) M N] [Algebra C S] :
          Algebra (ExactConstantExtension C M S) (ExactConstantExtension C N S)

          The algebra structure underlying the S(X)-linear tensor map. Its underlying ring homomorphism is the same tensor map as exactConstantExtensionTowerAlgebra; the separate name records the intended canonical rational-function-field interface.

          Equations
          Instances For
            source
            theorem BGS.HasseWeil.exactConstantExtensionTower_ratFuncScalarTower (C : Type u_1) (M : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field M] [Field N] [Field S] [Algebra (RatFunc C) M] [Algebra (RatFunc C) N] [Algebra M N] [IsScalarTower (RatFunc C) M N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExactN : algebraicClosure C N = ⊥) :
            have hExactM := ⋯; let E_M := ExactConstantExtension C M S; let E_N := ExactConstantExtension C N S; IsScalarTower (RatFunc S) E_M E_N

            The canonical S(X)-algebras on the two exact constant extensions and the tensor inclusion form a scalar tower.