Complete splitting in composita

Complete splitting in an intermediate field of a finite Galois extension means that every upstairs decomposition group fixes that intermediate field pointwise. Since the fixing subgroup of a compositum is the intersection of the fixing subgroups, complete splitting passes to composita. Embedding a finite separable extension into its finite Galois closure removes the Galois hypothesis on the ambient field. A completely split rational place also certifies exactness of the constant field of the compositum.

The decomposition-group argument follows the number-field analogue in TauCeti/NumberTheory/NumberField/SplitsCompletely/GaloisClosure.lean, using the place-theoretic fundamental identity and multiplicativity of ramification and residue degrees instead of ideals.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Corollary 3.9.7.

@[simp]

theorem TauCeti.Place.isSplitCompletely_sup_iff {k : Type u} {F : Type v} {M : Type w} [Field k] [Field F] [Field M] [Algebra k F] [Algebra k M] [Algebra F M] [IsScalarTower k F M] [FiniteDimensional F M] [Algebra.IsSeparable F M] (hF : IsFunctionField k F) (P : Place k F) (E₁ E₂ : IntermediateField F M) : P.IsSplitCompletely ↔ P.IsSplitCompletely ∧ P.IsSplitCompletely

Complete splitting in a compositum (Stichtenoth, Corollary 3.9.7). For intermediate fields of any finite separable extension, a place splits completely in their compositum if and only if it splits completely in each constituent. No rationality, perfectness, or exact-constants hypothesis is needed for this equivalence.

theorem TauCeti.Place.isIntegrallyClosedIn_sup_of_isSplitCompletely {k : Type u} {F : Type v} {M : Type w} [Field k] [Field F] [Field M] [Algebra k F] [Algebra k M] [Algebra F M] [IsScalarTower k F M] [FiniteDimensional F M] [Algebra.IsSeparable F M] (hF : IsFunctionField k F) (P : Place k F) (hP : P.degree = 1) (E₁ E₂ : IntermediateField F M) (h₁ : P.IsSplitCompletely) (h₂ : P.IsSplitCompletely) : IsIntegrallyClosedIn k ↥(E₁ ⊔ E₂)

If a rational place splits completely in both constituents, their compositum has exact constant field k (Stichtenoth, Corollary 3.9.7).