Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ConstantTensorResidue

Residue fields of constant tensor extensions #

For a maximal ideal q of S ⊗[C] R, let p be its contraction to R. Reduction gives a canonical map

S ⊗[C] κ(p) → κ(q).

This file proves that the map is surjective. For finite fields, the residue degree is therefore the least common multiple of the degrees of S and κ(p) over C. The result is ring-theoretic; applying it to places in a constant extension additionally requires identifying the normalization after base change with the corresponding tensor ring.

source
@[reducible, inline]
abbrev BGS.HasseWeil.ConstantTensorRing (C : Type u_1) (R : Type u_2) (S : Type u_3) [CommRing C] [CommRing R] [CommRing S] [Algebra C R] [Algebra C S] :
Type (max u_3 u_2)

The scalar extension of a commutative C-algebra R to a commutative C-algebra S.

Equations
Instances For
    source
    @[instance_reducible]
    def BGS.HasseWeil.constantTensorRingAlgebra (C : Type u_1) (R : Type u_2) (S : Type u_3) [CommRing C] [CommRing R] [CommRing S] [Algebra C R] [Algebra C S] :
    Algebra R (ConstantTensorRing C R S)

    The algebra structure from R to (ConstantTensorRing C R S) used in the constant tensor residue construction.

    Equations
    Instances For
      source
      noncomputable def BGS.HasseWeil.constantTensorResidueAlgHom (C : Type u_1) (R : Type u_2) (S : Type u_3) [CommRing C] [CommRing R] [CommRing S] [Algebra C R] [Algebra C S] (q : Ideal (ConstantTensorRing C R S)) [q.IsMaximal] :
      let p := Ideal.comap Algebra.TensorProduct.includeRight.toRingHom q; TensorProduct C S p.ResidueField →ₐ[C] q.ResidueField

      The canonical map from the tensor product of the enlarged constants and the contracted residue field to the upstairs residue field.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem BGS.HasseWeil.constantTensorResidueAlgHom_surjective (C : Type u_1) (R : Type u_2) (S : Type u_3) [CommRing C] [CommRing R] [CommRing S] [Algebra C R] [Algebra C S] (q : Ideal (ConstantTensorRing C R S)) [q.IsMaximal] :
        Function.Surjective ⇑(constantTensorResidueAlgHom C R S q)

        The canonical residue-field map of a constant tensor extension is surjective.

        source
        @[instance_reducible]
        def BGS.HasseWeil.finiteConstantTensorRingAlgebra (C : Type u_1) (R : Type u_2) (S : Type u_3) [Field C] [CommRing R] [Field S] [Algebra C R] [Algebra C S] :
        Algebra R (ConstantTensorRing C R S)

        The algebra structure from R to (ConstantTensorRing C R S) used in the constant tensor residue construction.

        Equations
        Instances For
          source
          theorem BGS.HasseWeil.constantTensorResidue_finrank_eq_lcm (C : Type u_1) (R : Type u_2) (S : Type u_3) [Field C] [CommRing R] [Field S] [Algebra C R] [Algebra C S] (q : Ideal (ConstantTensorRing C R S)) [q.IsMaximal] [Finite C] [Finite S] [Finite (Ideal.comap Algebra.TensorProduct.includeRight.toRingHom q).ResidueField] [Finite q.ResidueField] :
          let p := Ideal.comap Algebra.TensorProduct.includeRight.toRingHom q; Module.finrank C q.ResidueField = (Module.finrank C S).lcm (Module.finrank C p.ResidueField)

          For finite fields, the residue field of a constant tensor extension has degree equal to the least common multiple of the new-constant degree and the contracted residue degree.