Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FiniteFieldPolynomialNormalization

Normalization after finite constant extension #

Smooth base change commutes with integral closure. Applied to the coefficient extension C[X] → S[X], this identifies the base change of the normalization of a C[X]-algebra with the normalization of its polynomial base change.

The first declaration records the general smooth statement. The second specializes it to finite fields: finiteness makes S / C finite type, while the perfectness of C supplies formal smoothness.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.finiteFieldNormalizationPolynomialCoefficientAlgebra (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 polynomial normalization construction.

Equations
Instances For
    source
    noncomputable def BGS.HasseWeil.polynomialIntegralClosureBaseChangeAlgEquiv (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.Smooth C S] :
    TensorProduct (Polynomial C) (Polynomial S) ↥(integralClosure (Polynomial C) N) ≃ₐ[Polynomial S] ↥(integralClosure (Polynomial S) (TensorProduct (Polynomial C) (Polynomial S) N))

    Smooth coefficient extension commutes with normalization over the polynomial base.

    Equations
    Instances For
      source
      noncomputable def BGS.HasseWeil.finiteFieldPolynomialIntegralClosureBaseChangeAlgEquiv (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] [Fintype C] [Finite S] :
      TensorProduct (Polynomial C) (Polynomial S) ↥(integralClosure (Polynomial C) N) ≃ₐ[Polynomial S] ↥(integralClosure (Polynomial S) (TensorProduct (Polynomial C) (Polynomial S) N))

      For an extension of finite fields, coefficient extension commutes with normalization over the polynomial base.

      Equations
      Instances For