Normalization in a finite constant extension

Let N be a C[X]-algebra and let S / C be a finite extension of finite fields. Combining smooth base change for integral closure with explicit polynomial tensor cancellation gives

S ⊗[C] integralClosure C[X] N ≃ integralClosure S[X] (S ⊗[C] N).

The normalization comparison is first kept over S[X], so it transports contractions of height-one primes to the polynomial base. Its restriction to S is retained for residue-field dimension calculations. The values of both equivalences on pure tensors are recorded explicitly.

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalizationBaseConstantAlgebra (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 normalization construction.

Equations

• BGS.HasseWeil.normalizationBaseConstantAlgebra C N = ((algebraMap (Polynomial C) N).comp (algebraMap C (Polynomial C))).toAlgebra

theorem BGS.HasseWeil.normalizationBaseConstantPolynomialTower (C : Type u_1) (N : Type u_3) [Field C] [CommRing N] [Algebra (Polynomial C) N] : IsScalarTower C (Polynomial C) N

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalizationCoefficientPolynomialAlgebra (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 normalization construction.

Equations

• BGS.HasseWeil.normalizationCoefficientPolynomialAlgebra C S = Polynomial.algebra C S

@[reducible]

noncomputable def BGS.HasseWeil.constantExtensionTensorPolynomialAlgebra (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 polynomial algebra structure on the constant-extended ambient ring. It sends X to 1 ⊗ algebraMap C[X] N X. This public name lets downstream function-field constructions install exactly the same algebra structure.

Equations

• BGS.HasseWeil.constantExtensionTensorPolynomialAlgebra C S N = BGS.HasseWeil.polynomialTensorCancelTargetPolynomialExtensionAlgebra C S N

@[reducible]

noncomputable def BGS.HasseWeil.constantExtensionNormalizationTensorPolynomialAlgebra (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 ↥(integralClosure (Polynomial C) N))

The matching polynomial algebra structure on the constant tensor of the original normalization.

Equations

• BGS.HasseWeil.constantExtensionNormalizationTensorPolynomialAlgebra C S N = BGS.HasseWeil.polynomialTensorCancelTargetPolynomialExtensionAlgebra C S ↥(integralClosure (Polynomial C) N)

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalizationTargetPolynomialAlgebra (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 normalization construction.

Equations

• BGS.HasseWeil.normalizationTargetPolynomialAlgebra C S N = BGS.HasseWeil.constantExtensionTensorPolynomialAlgebra C S N

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalizationSourcePolynomialAlgebra (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 ↥(integralClosure (Polynomial C) N))

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

Equations

• BGS.HasseWeil.normalizationSourcePolynomialAlgebra C S N = BGS.HasseWeil.constantExtensionNormalizationTensorPolynomialAlgebra C S N

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalizationTargetConstantAlgebra (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 normalization construction.

Equations

• BGS.HasseWeil.normalizationTargetConstantAlgebra C S N = Algebra.TensorProduct.leftAlgebra

theorem BGS.HasseWeil.normalizationTargetConstantPolynomialTower (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)

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalizationTargetIntegralClosureConstantAlgebra (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 normalization construction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosurePolynomialAlgEquiv (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 C S ↥(integralClosure (Polynomial C) N) ≃ₐ[Polynomial S] ↥(integralClosure (Polynomial S) (TensorProduct C S N))

After a finite extension of finite constants, normalization commutes with constant extension as an equivalence over the polynomial ring S[X].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosurePolynomialAlgEquiv_tmul (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] (s : S) (a : ↥(integralClosure (Polynomial C) N)) : ↑((finiteFieldConstantExtensionIntegralClosurePolynomialAlgEquiv C S N) (s ⊗ₜ[C] a)) = s ⊗ₜ[C] ↑a

The polynomial-algebra normalization equivalence sends a pure tensor to the corresponding pure tensor in the extended ambient algebra.

noncomputable def BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosureAlgEquiv (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 C S ↥(integralClosure (Polynomial C) N) ≃ₐ[S] ↥(integralClosure (Polynomial S) (TensorProduct C S N))

After a finite extension of finite constants, the normalization is the constant tensor extension of the original normalization.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosureAlgEquiv_tmul (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] (s : S) (a : ↥(integralClosure (Polynomial C) N)) : ↑((finiteFieldConstantExtensionIntegralClosureAlgEquiv C S N) (s ⊗ₜ[C] a)) = s ⊗ₜ[C] ↑a

The normalization equivalence sends a pure tensor to the corresponding pure tensor in the extended function algebra.

noncomputable def BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosureRingEquiv (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 C S ↥(integralClosure (Polynomial C) N) ≃+* ↥(integralClosure (Polynomial S) (TensorProduct C S N))

The normalization comparison with its constant-algebra structures erased. This is the stable interface for constructions that only need the underlying ring map and should not depend on the particular S-algebra instances used to build the comparison.

Equations

• BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosureRingEquiv C S N = (BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosureAlgEquiv C S N).toRingEquiv

@[simp]

theorem BGS.HasseWeil.finiteFieldConstantExtensionIntegralClosureRingEquiv_tmul (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] (s : S) (a : ↥(integralClosure (Polynomial C) N)) : ↑((finiteFieldConstantExtensionIntegralClosureRingEquiv C S N) (s ⊗ₜ[C] a)) = s ⊗ₜ[C] ↑a

The instance-free normalization comparison has the expected value on a pure tensor.