Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FiniteFieldConstantExtensionResidue

Residue degrees after finite constant extension #

This file transports the abstract residue-tensor calculation across the normalization equivalence. If q is a maximal ideal of the normalization after extending finite constants from C to S, and p is its contraction to the old normalization, then

[κ(q) : C] = lcm([S : C], [κ(p) : C])

and hence

[κ(q) : S] = [κ(p) : C] / gcd([S : C], [κ(p) : C]).

In particular, q is rational over S whenever the downstairs residue degree divides [S : C].

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.constantExtensionResidueBaseConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [CommRing N] [Algebra (Polynomial C) N] :
Algebra C N

The algebra structure from C to N used in the finite field constant extension residue construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.constantExtensionResidueBaseConstantPolynomialTower (C : Type u_1) (N : Type u_3) [Field C] [CommRing N] [Algebra (Polynomial C) N] :
    IsScalarTower C (Polynomial C) N
    source
    @[instance_reducible]
    noncomputable def BGS.HasseWeil.constantExtensionResidueCoefficientPolynomialAlgebra (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] :
    Algebra (Polynomial C) (Polynomial S)

    The algebra structure from C[X] to S[X] used in the finite field constant extension residue construction.

    Equations
    Instances For
      source
      @[instance_reducible]
      noncomputable def BGS.HasseWeil.constantExtensionResidueOldNormalizationConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [CommRing N] [Algebra (Polynomial C) N] :
      Algebra C ↥(integralClosure (Polynomial C) N)

      The algebra structure from C to (integralClosure C[X] N) used in the finite field constant extension residue construction.

      Equations
      Instances For
        source
        @[instance_reducible]
        noncomputable def BGS.HasseWeil.constantExtensionResidueTargetPolynomialAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [CommRing N] [Algebra (Polynomial C) N] :
        Algebra (Polynomial S) (TensorProduct C S N)

        The algebra structure from S[X] to (S ⊗[C] N) used in the finite field constant extension residue construction.

        Equations
        Instances For
          source
          @[instance_reducible]
          noncomputable def BGS.HasseWeil.constantExtensionResidueTargetConstantAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [CommRing N] [Algebra (Polynomial C) N] :
          Algebra S (TensorProduct C S N)

          The algebra structure from S to (S ⊗[C] N) used in the finite field constant extension residue construction.

          Equations
          Instances For
            source
            theorem BGS.HasseWeil.constantExtensionResidueTargetConstantPolynomialTower (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [CommRing N] [Algebra (Polynomial C) N] :
            IsScalarTower S (Polynomial S) (TensorProduct C S N)
            source
            @[instance_reducible]
            noncomputable def BGS.HasseWeil.constantExtensionResidueTargetNormalizationConstantAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [CommRing N] [Algebra (Polynomial C) N] :
            Algebra S ↥(integralClosure (Polynomial S) (TensorProduct C S N))

            The algebra structure from S to (integralClosure S[X] (S ⊗[C] N)) used in the finite field constant extension residue construction.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              noncomputable def BGS.HasseWeil.constantExtensionResidueTargetNormalizationBaseAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [CommRing N] [Algebra (Polynomial C) N] :
              Algebra C ↥(integralClosure (Polynomial S) (TensorProduct C S N))

              The algebra structure from C to (integralClosure S[X] (S ⊗[C] N)) used in the finite field constant extension residue construction.

              Equations
              Instances For
                source
                theorem BGS.HasseWeil.constantExtensionResidueTargetNormalizationConstantTower (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [CommRing N] [Algebra (Polynomial C) N] :
                IsScalarTower C S ↥(integralClosure (Polynomial S) (TensorProduct C S N))
                source
                noncomputable def BGS.HasseWeil.finiteFieldConstantExtensionTensorIdeal (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) :
                Ideal (TensorProduct C S ↥(integralClosure (Polynomial C) N))

                Pull a maximal ideal of the base-changed normalization back to the tensor model of that normalization.

                Equations
                Instances For
                  source
                  noncomputable def BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosureAlgHom (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] :
                  ↥(integralClosure (Polynomial C) N) →ₐ[C] ↥(integralClosure (Polynomial S) (TensorProduct C S N))

                  The inclusion of the old normalization into the normalization after constant extension.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosureRingHom (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] :
                    ↥(integralClosure (Polynomial C) N) →+* ↥(integralClosure (Polynomial S) (TensorProduct C S N))

                    Ring-homomorphism form of the old-normalization inclusion.

                    Equations
                    Instances For
                      source
                      noncomputable def BGS.HasseWeil.finiteFieldConstantExtensionDownstairsIdeal (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) :
                      Ideal ↥(integralClosure (Polynomial C) N)

                      Contract an upstairs maximal ideal to the old normalization.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem BGS.HasseWeil.finiteFieldConstantExtensionDownstairsIdeal_eq (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) :
                        finiteFieldConstantExtensionDownstairsIdeal C S N q = Ideal.comap Algebra.TensorProduct.includeRight.toRingHom (finiteFieldConstantExtensionTensorIdeal C S N q)
                        source
                        @[simp]
                        theorem BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosureRingHom_coe (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (a : ↥(integralClosure (Polynomial C) N)) :
                        ↑((finiteFieldConstantExtensionIntegralClosureRingHom C S N) a) = 1 ⊗ₜ[C] ↑a
                        source
                        theorem BGS.HasseWeil.finiteFieldConstantExtensionTensorIdeal_isMaximal (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) [q.IsMaximal] :
                        (finiteFieldConstantExtensionTensorIdeal C S N q).IsMaximal
                        source
                        theorem BGS.HasseWeil.finiteFieldConstantExtensionDownstairsIdeal_isPrime (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) [q.IsMaximal] :
                        (finiteFieldConstantExtensionDownstairsIdeal C S N q).IsPrime
                        source
                        noncomputable def BGS.HasseWeil.finiteFieldConstantExtensionResidueFieldAlgEquiv (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) [q.IsMaximal] :
                        (finiteFieldConstantExtensionTensorIdeal C S N q).ResidueField ≃ₐ[S] q.ResidueField

                        The normalization equivalence induces an S-algebra equivalence of the corresponding residue fields.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem BGS.HasseWeil.finiteFieldConstantExtensionTensorResidueFinite (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) [q.IsMaximal] [Finite q.ResidueField] :
                          Finite (finiteFieldConstantExtensionTensorIdeal C S N q).ResidueField
                          source
                          theorem BGS.HasseWeil.finiteFieldConstantExtensionDownstairsResidueFinite (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) [q.IsMaximal] [Finite q.ResidueField] :
                          Finite (finiteFieldConstantExtensionDownstairsIdeal C S N q).ResidueField
                          source
                          theorem BGS.HasseWeil.finiteFieldConstantExtensionDownstairsIdeal_isMaximal (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) [q.IsMaximal] [Finite q.ResidueField] :
                          (finiteFieldConstantExtensionDownstairsIdeal C S N q).IsMaximal

                          The contraction of an upstairs maximal ideal is maximal. The proof uses the already established embedding of its residue field into the finite upstairs residue field: the downstairs quotient is therefore a finite domain, and hence a field.

                          source
                          theorem BGS.HasseWeil.finiteFieldConstantExtensionResidue_finrank_eq_lcm (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) [q.IsMaximal] [Finite q.ResidueField] :
                          Module.finrank C q.ResidueField = (Module.finrank C S).lcm (Module.finrank C (finiteFieldConstantExtensionDownstairsIdeal C S N q).ResidueField)

                          Absolute residue-degree form of the constant-extension compositum formula.

                          source
                          theorem BGS.HasseWeil.finiteFieldConstantExtensionResidue_finrank_over_constants_eq_div_gcd (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) [q.IsMaximal] [Finite q.ResidueField] :
                          Module.finrank S q.ResidueField = Module.finrank C (finiteFieldConstantExtensionDownstairsIdeal C S N q).ResidueField / (Module.finrank C S).gcd (Module.finrank C (finiteFieldConstantExtensionDownstairsIdeal C S N q).ResidueField)

                          Relative residue-degree form of the constant-extension compositum formula.

                          source
                          theorem BGS.HasseWeil.finiteFieldConstantExtensionResidue_finrank_eq_one_of_dvd (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Algebra C S] [Fintype C] [Finite S] [CommRing N] [Algebra (Polynomial C) N] (q : Ideal ↥(integralClosure (Polynomial S) (TensorProduct C S N))) [q.IsMaximal] [Finite q.ResidueField] (hdiv : Module.finrank C (finiteFieldConstantExtensionDownstairsIdeal C S N q).ResidueField ∣ Module.finrank C S) :
                          Module.finrank S q.ResidueField = 1

                          If the downstairs residue degree divides the constant-extension degree, then the upstairs maximal ideal has residue degree one over the enlarged constants.