The exact constant-extension tower of a function-field normal closure

Let F / K(X) have exact constant field K, let N be the chosen normal closure, let C be the full algebraic constant field of N, and let M = CF ⊆ N be the original compositum. For a finite Galois extension S / C, this file specializes the generic exact-constant-extension tower to

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

It packages the canonical S(X)-linear inclusion, the finite Galois structure of the top over the bottom, and preservation of both the relative degree and the two rational-function-field degrees. This is a structural consumer of the exact constant-extension API; it deliberately does not use the genus-invariance layer.

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalClosureTowerBaseConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C N

The algebra structure from C to N used in the exact constant extension normal closure tower construction.

Equations

• BGS.HasseWeil.normalClosureTowerBaseConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

theorem BGS.HasseWeil.normalClosureTowerBaseConstantTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (RatFunc C) N

@[reducible]

noncomputable instance BGS.HasseWeil.functionFieldNormalClosureConstantBaseConstantRatFuncAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] : Algebra (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosureConstantBase K F)

The C(X)-algebra on the constant-base field C K(X), transported through its canonical rational-function presentation.

Equations

• BGS.HasseWeil.functionFieldNormalClosureConstantBaseConstantRatFuncAlgebra K F = (↑(BGS.HasseWeil.functionFieldNormalClosureConstantBaseRatFuncAlgEquiv K F)).toAlgebra

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantBaseRatFuncSelfAlgEquiv (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] : RatFunc ↥(FunctionFieldNormalClosureConstantField K F) ≃ₐ[RatFunc ↥(FunctionFieldNormalClosureConstantField K F)] ↥(FunctionFieldNormalClosureConstantBase K F)

The canonical rational-function presentation of the constant-base field, viewed as an equivalence over C(X) itself.

Equations

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

instance BGS.HasseWeil.functionFieldNormalClosureConstantBase_finiteDimensional_over_constantRatFunc (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] : FiniteDimensional (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosureConstantBase K F)

The constant-base field is one-dimensional, hence finite, over its canonical C(X) presentation.

@[reducible]

noncomputable instance BGS.HasseWeil.functionFieldNormalClosureConstantRatFuncAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] : Algebra (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosure K F)

The canonical C(X)-algebra on the normal closure, obtained by including the constant-base field C K(X) into the normal closure.

Equations

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

instance BGS.HasseWeil.functionFieldNormalClosureConstantRatFuncBaseTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] : IsScalarTower (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosureConstantBase K F) ↥(FunctionFieldNormalClosure K F)

The canonical C(X) map to the normal closure factors through the constant-base field.

instance BGS.HasseWeil.functionFieldNormalClosure_finiteDimensional_over_constantRatFunc (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] : FiniteDimensional (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosure K F)

The normal closure is finite over the canonical copy of C(X).

theorem BGS.HasseWeil.functionFieldNormalClosure_isGalois_over_constantRatFunc (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] : IsGalois (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosure K F)

The normal closure remains Galois after replacing the constant-base fixed field by its canonical rational-function presentation C(X).

theorem BGS.HasseWeil.functionFieldNormalClosureConstantField_isExact_for_constantRatFunc (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] : let C := FunctionFieldNormalClosureConstantField K F; let N := FunctionFieldNormalClosure K F; algebraicClosure ↥C ↥N = ⊥

Exactness of the full normal-closure constant field, stated for the constant algebra obtained by restricting the canonical C(X) presentation. This is the exact instance expected by the generic tower API.

@[reducible]

noncomputable instance BGS.HasseWeil.functionFieldNormalClosureConstantBaseOriginalCompositumAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) : Algebra ↥(FunctionFieldNormalClosureConstantBase K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

The constant-base field embeds into the original compositum CF.

Equations

• BGS.HasseWeil.functionFieldNormalClosureConstantBaseOriginalCompositumAlgebra K F hExact = (BGS.HasseWeil.functionFieldNormalClosureConstantBaseToOriginalCompositum K F hExact).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.constantBaseOriginalCompositumSmul (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) : SMul ↥(FunctionFieldNormalClosureConstantBase K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

The scalar action of (FunctionFieldNormalClosureConstantBase K F) on (FunctionFieldNormalClosureOriginalCompositum K F hExact) used in the exact constant extension normal closure tower construction.

Equations

• BGS.HasseWeil.constantBaseOriginalCompositumSmul K F hExact = (BGS.HasseWeil.functionFieldNormalClosureConstantBaseOriginalCompositumAlgebra K F hExact).toSMul

@[instance_reducible]

noncomputable def BGS.HasseWeil.constantBaseOriginalCompositumModule (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) : Module ↥(FunctionFieldNormalClosureConstantBase K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

The module structure of (FunctionFieldNormalClosureOriginalCompositum K F hExact) over (FunctionFieldNormalClosureConstantBase K F) used in the exact constant extension normal closure tower construction.

Equations

• BGS.HasseWeil.constantBaseOriginalCompositumModule K F hExact = Algebra.toModule

instance BGS.HasseWeil.functionFieldNormalClosureConstantBaseOriginalCompositumTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) : IsScalarTower ↥(FunctionFieldNormalClosureConstantBase K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact) ↥(FunctionFieldNormalClosure K F)

The embeddings of the constant base into CF and then into the normal closure agree with its direct inclusion.

instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantRatFuncBaseTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) : IsScalarTower (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosureConstantBase K F) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

The existing C(X) structure on CF factors through the constant-base field.

instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantRatFuncTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) : IsScalarTower (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact) ↥(FunctionFieldNormalClosure K F)

The canonical C(X) structures on CF and on the normal closure are compatible with the inclusion CF ⊆ N.

instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositum_finiteDimensional_over_constantRatFunc (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) : FiniteDimensional (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

The original compositum is finite over its canonical copy of C(X).

@[instance_reducible]

noncomputable def BGS.HasseWeil.canonicalOriginalConstantAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] : Algebra K F

The algebra structure from K to F used in the exact constant extension normal closure tower construction.

Equations

• BGS.HasseWeil.canonicalOriginalConstantAlgebra K F = BGS.HasseWeil.functionFieldCanonicalConstantAlgebra K F

theorem BGS.HasseWeil.canonicalOriginalConstantTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] : IsScalarTower K (RatFunc K) F

theorem BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantField_isExact_for_constantRatFunc (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; algebraicClosure ↥C ↥M = ⊥

In the canonical C(X) presentation, C is also the exact constant field of the original compositum CF.

instance BGS.HasseWeil.functionFieldNormalClosureOriginalCompositum_isSeparable_over_constantRatFunc (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) : Algebra.IsSeparable (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosureOriginalCompositum K F hExact)

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalClosureConstantExtensionModule (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] : Module (↥(FunctionFieldNormalClosureConstantField K F)) S

The module structure of S over (FunctionFieldNormalClosureConstantField K F) used in the exact constant extension normal closure tower construction.

Equations

• BGS.HasseWeil.normalClosureConstantExtensionModule K F S = Algebra.toModule

@[reducible]

noncomputable def BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantExtensionField (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; Field (ExactConstantExtension (↥C) (↥M) S)

The field structure on S ⊗[C] CF used by the normal-closure tower.

Equations

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

@[reducible]

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantExtensionFieldForTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] : let C := FunctionFieldNormalClosureConstantField K F; let N := FunctionFieldNormalClosure K F; Field (ExactConstantExtension (↥C) (↥N) S)

The field structure on S ⊗[C] N in the same canonical C(X) presentation.

Equations

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

@[reducible]

noncomputable def BGS.HasseWeil.functionFieldNormalClosureOriginalCompositumConstantExtensionRatFuncAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; Algebra (RatFunc S) (ExactConstantExtension (↥C) (↥M) S)

The canonical S(X)-algebra on S ⊗[C] CF.

Equations

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

@[reducible]

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantExtensionRatFuncAlgebraForTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] : let C := FunctionFieldNormalClosureConstantField K F; let N := FunctionFieldNormalClosure K F; Algebra (RatFunc S) (ExactConstantExtension (↥C) (↥N) S)

The canonical S(X)-algebra on S ⊗[C] N.

Equations

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

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantExtensionTowerAlgHom (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; let N := FunctionFieldNormalClosure K F; let E_M := ExactConstantExtension (↥C) (↥M) S; let E_N := ExactConstantExtension (↥C) (↥N) S; E_M →ₐ[RatFunc S] E_N

The canonical S(X)-linear inclusion S ⊗[C] CF → S ⊗[C] N.

Equations

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

@[reducible]

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantExtensionTowerAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; let N := FunctionFieldNormalClosure K F; Algebra (ExactConstantExtension (↥C) (↥M) S) (ExactConstantExtension (↥C) (↥N) S)

The algebra structure underlying the specialized tensor inclusion.

Equations

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

theorem BGS.HasseWeil.functionFieldNormalClosureConstantExtension_ratFuncScalarTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; let N := FunctionFieldNormalClosure K F; let E_M := ExactConstantExtension (↥C) (↥M) S; let E_N := ExactConstantExtension (↥C) (↥N) S; IsScalarTower (RatFunc S) E_M E_N

The specialized inclusion and the canonical S(X) structures form a scalar tower.

theorem BGS.HasseWeil.functionFieldNormalClosureConstantExtension_finiteDimensional (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; let N := FunctionFieldNormalClosure K F; let E_M := ExactConstantExtension (↥C) (↥M) S; let E_N := ExactConstantExtension (↥C) (↥N) S; Module.Finite E_M E_N

The extended normal closure is finite-dimensional over the extended original compositum.

theorem BGS.HasseWeil.functionFieldNormalClosureConstantExtension_isGalois (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; let N := FunctionFieldNormalClosure K F; let E_M := ExactConstantExtension (↥C) (↥M) S; let E_N := ExactConstantExtension (↥C) (↥N) S; IsGalois E_M E_N

The extended normal closure remains Galois over the extended original compositum.

theorem BGS.HasseWeil.functionFieldNormalClosureConstantExtension_finrank (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; let N := FunctionFieldNormalClosure K F; let E_M := ExactConstantExtension (↥C) (↥M) S; let E_N := ExactConstantExtension (↥C) (↥N) S; Module.finrank E_M E_N = Module.finrank ↥M ↥N

Extending the full constant field preserves the degree of the normal closure over the original compositum.

theorem BGS.HasseWeil.functionFieldNormalClosureConstantExtension_card_aut_eq (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; let N := FunctionFieldNormalClosure K F; let E_M := ExactConstantExtension (↥C) (↥M) S; let E_N := ExactConstantExtension (↥C) (↥N) S; Nat.card (E_N ≃ₐ[E_M] E_N) = Nat.card Gal(↥N/↥M)

Consequently the specialized tower Galois group has the same cardinality as the normal-closure group over the original compositum.

theorem BGS.HasseWeil.normalClosureOriginalCompositum_rationalPlaceCount_eq_exactExtensionCount (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let C := FunctionFieldNormalClosureConstantField K F; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; have hExactM := ⋯; let E_M := ExactConstantExtension (↥C) (↥M) S; finiteExtensionRationalPlaceCount S E_M = exactConstantExtensionClosedPlaceExtensionCount (↥C) S (↥M) hExactM 1

The rational-place count of the extended original compositum is the packaged level-one exact constant-extension count of that compositum.

theorem BGS.HasseWeil.normalClosureOriginalCompositum_rationalPlaceCount_eq_originalExactExtensionCount (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Fintype K] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K F)) S] [Module.Finite (↥(FunctionFieldNormalClosureConstantField K F)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K F)) S] (hExact : algebraicClosure K F = ⊥) : let N := FunctionFieldNormalClosure K F; let this := functionFieldNormalClosureConstantAlgebra K F; let C := FunctionFieldNormalClosureConstantField K F; let this := SubalgebraClass.toAlgebra (algebraicClosure K ↥N); have this_1 := ⋯; have this_2 := ⋯; let M := FunctionFieldNormalClosureOriginalCompositum K F hExact; let this_3 := functionFieldNormalClosureOriginalCompositumConstantRatFuncAlgebra K F hExact; let this_4 := exactConstantExtensionTowerCanonicalConstantAlgebra ↥C ↥M; have hExactM := ⋯; let E_M := ExactConstantExtension (↥C) (↥M) S; let this_5 := functionFieldNormalClosureOriginalCompositumConstantExtensionField K F S hExact; let this_6 := functionFieldNormalClosureOriginalCompositumConstantExtensionRatFuncAlgebra K F S hExact; let this_7 := Algebra.toModule; have this_8 := ⋯; have this_9 := ⋯; have this_10 := ⋯; have this_11 := Fintype.ofFinite ↥C; have this_12 := ⋯; have this_13 := Fintype.ofFinite S; have this_14 := Classical.decEq ↥C; have this_15 := Classical.decEq (RatFunc ↥C); have this_16 := Classical.decEq S; have this_17 := Classical.decEq (RatFunc S); finiteExtensionRationalPlaceCount S E_M = exactConstantExtensionClosedPlaceExtensionCount K (↥C) F hExact (Module.finrank (↥C) S)

Combining the exact splitting formula with the canonical C(X)-equivalence C ⊗[K] F ≃ CF identifies the same rational-place count with the packaged exact-extension count of the original function field at level [S : C].