Documentation

TauCeti.FieldTheory.FunctionField.Place.Extension.Splitting

Places that split completely in an extension of function fields #

Let F' / k' be a finite extension of F / k. A place P of F / k splits completely when it has [F' : F] distinct extensions to F' / k', the largest number allowed by the fundamental inequality. This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Definition 3.1.13.

For a separable extension, the fundamental identity

sum_{P' | P} e(P' | P) * f(P' | P) = [F' : F]

shows that complete splitting is equivalent to every place above P having ramification index and relative degree both equal to one. In the Galois case these invariants are constant on the fibre, so it is enough to check either one place above P. Equivalently, the decomposition group of such a place is trivial.

Main definitions #

Main results #

Provenance #

The orbit--stabilizer proof of the Galois criterion follows the existing number-field analogue NumberField.ncard_primesOver_eq_finrank_iff_stabilizer_eq_bot in TauCeti/NumberTheory/NumberField/SplitsCompletely/Basic.lean. The non-Galois criterion is proved directly from the function-field fundamental identity.

References #

source
def TauCeti.Place.IsSplitCompletely {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (P : Place k F) :
Prop

A place P of F / k splits completely in F' / k' if it has [F' : F] distinct extensions to F' / k' (Stichtenoth, Definition 3.1.13). This is the maximal possible cardinality by TauCeti.Place.ncard_setOf_restrict_eq_le_finrank.

Equations
Instances For
    source
    theorem TauCeti.Place.isSplitCompletely_iff {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (P : Place k F) :
    P.IsSplitCompletely ↔ FiniteDimensional F F' ∧ {P' : Place k' F' | restrict k F P' = P}.ncard = Module.finrank F F'

    The characteristic property of a place splitting completely.

    source
    theorem TauCeti.Place.isSplitCompletely_def {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [FiniteDimensional F F'] (P : Place k F) :
    P.IsSplitCompletely ↔ {P' : Place k' F' | restrict k F P' = P}.ncard = Module.finrank F F'

    The definition of a place splitting completely, restated for rewriting.

    source
    theorem TauCeti.Place.not_isSplitCompletely_iff_ncard_lt {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [FiniteDimensional F F'] (P : Place k F) :
    ¬P.IsSplitCompletely ↔ {P' : Place k' F' | restrict k F P' = P}.ncard < Module.finrank F F'

    A place does not split completely exactly when the number of places above it is strictly smaller than the extension degree.

    source
    theorem TauCeti.Place.IsSplitCompletely.ramificationIdx_eq_one {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [FiniteDimensional F F'] {P : Place k F} (hP : P.IsSplitCompletely) {P' : Place k' F'} (hP' : restrict k F P' = P) :
    ramificationIdx F P' = 1

    A place above a completely split place has ramification index one.

    source
    theorem TauCeti.Place.IsSplitCompletely.relativeDegree_eq_one {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [FiniteDimensional F F'] {P : Place k F} (hP : P.IsSplitCompletely) {P' : Place k' F'} (hP' : restrict k F P' = P) :
    relativeDegree k F P' = 1

    A place above a completely split place has relative residue degree one.

    source
    theorem TauCeti.Place.IsSplitCompletely.bijective_algebraMap_residueField {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [FiniteDimensional F F'] (P' : Place k' F') (hP : (restrict k F P').IsSplitCompletely) :
    Function.Bijective ⇑(algebraMap (restrict k F P').ResidueField P'.ResidueField)

    At a place above a completely split place, the map between residue fields is bijective.

    source
    theorem TauCeti.Place.isSplitCompletely_iff_forall_ramificationIdx_eq_one_and_relativeDegree_eq_one {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [FiniteDimensional F F'] [Algebra.IsIntegral k k'] [Algebra.IsSeparable F F'] (P : Place k F) :
    P.IsSplitCompletely ↔ ∀ (P' : Place k' F'), restrict k F P' = P → ramificationIdx F P' = 1 ∧ relativeDegree k F P' = 1

    Complete splitting is equivalent to trivial ramification and residue extensions at every place above P (Stichtenoth, Definition 3.1.13 and Theorem 3.1.11).

    No Galois hypothesis is needed: if the number of summands in the fundamental identity already equals [F' : F], then every positive summand e(P' | P) * f(P' | P) must equal one.

    source
    theorem TauCeti.Place.isSplitCompletely_iff_ramificationIdx_eq_one_and_relativeDegree_eq_one {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [FiniteDimensional F F'] [IsGalois F F'] (P' : Place k F') :
    (restrict k F P').IsSplitCompletely ↔ ramificationIdx F P' = 1 ∧ relativeDegree k F P' = 1

    In a finite Galois extension, one place detects complete splitting (Stichtenoth, Corollary 3.7.2): the place below P' splits completely exactly when the common ramification index and relative degree on its fibre are both one.

    source
    theorem TauCeti.Place.isSplitCompletely_iff_stabilizer_eq_bot {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [FiniteDimensional F F'] [IsGalois F F'] (P' : Place k F') :
    (restrict k F P').IsSplitCompletely ↔ MulAction.stabilizer Gal(F'/F) P' = ⊥

    Complete splitting is equivalent to a trivial stabilizer in a finite Galois extension. The fibre of restriction is the orbit of P', so this is the orbit--stabilizer form of complete splitting.

    source
    theorem TauCeti.Place.isSplitCompletely_iff_decompositionSubgroup_eq_bot {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] [Algebra k F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] [FiniteDimensional F F'] [IsGalois F F'] (P' : Place k F') :
    (restrict k F P').IsSplitCompletely ↔ ValuationSubring.decompositionSubgroup F P'.integers = ⊥

    Complete splitting is equivalent to a trivial decomposition group in a finite Galois extension (Stichtenoth, Definitions 3.1.13 and 3.8.1).