Module

NormalClosure.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.Splitting.NormalClosure

30 declarations indexed from sourceView source ↗

Module documentation

Complete splitting and normal closures

This file formalizes the normal-closure reduction for complete splitting. For a finite Galois extension M / K, an intermediate field L, a nontrivial absolute value v of K, and an extension w to M, put

G = Gal(M / K),
H = Gal(M / L), and
D = D(w / v).

Restriction of the conjugates of w gives an equivalence

H \ G / D ≃ { extensions of v to L }.

Thus the intrinsic complete-splitting condition for the possibly non-Galois extension L / K is exactly the equality between the number of double cosets and the number of left cosets. If M is generated by the K-conjugates of L, then H has trivial normal core. SplittingGroupTheory consequently forces D = 1, so the place splits completely already in M.

Imports3

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.CyclicPrimeSubextension
Nyll.ClassFieldTheory.AlgebraicNumberTheory.NormalClosure
Mathlib.FieldTheory.Normal.Closure

Imported by5

def

extendAbsoluteValueExtensionFromIntermediate

L52 ↗

Documentation

Extend an actual extension of v from an intermediate field to the ambient finite Galois extension. The source is the absolute-value extension theorem, applied to the algebraic extension M / L.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section AbsoluteValueExtensions
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]

Lean source · statement

def extendAbsoluteValueExtensionFromIntermediate
    [FiniteDimensional K M]
    (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial)
    (L : IntermediateField K M)
    (u : AbsoluteValueExtension vK L) :
    AbsoluteValueExtension vK M

theorem

extendAbsoluteValueExtensionFromIntermediate_apply

L75 ↗

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section AbsoluteValueExtensions
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]

Lean source · statement

theorem extendAbsoluteValueExtensionFromIntermediate_apply
    [FiniteDimensional K M]
    (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial)
    (L : IntermediateField K M)
    (u : AbsoluteValueExtension vK L)
    (x : L) :
    (extendAbsoluteValueExtensionFromIntermediate
      vK hvK L u).1 x = u.1 x

def

doubleCosetExtension

L109 ↗

Documentation

The extension of v to L attached to a representative of H \ G / D. Inversion changes the natural D \ G / H convention for the right action w ↦ w ∘ σ into the convention used for the normal-closure reduction.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section AbsoluteValueExtensions
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
variable (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK M)
    (L : IntermediateField K M)
local notation "G" => M ≃ₐ[K] M
local notation "H" => L.fixingSubgroup
local notation "D" => absoluteValueDecompositionGroup K w.val

Lean source · statement

def doubleCosetExtension :
    DoubleCoset.Quotient (H : Set G) D →
      AbsoluteValueExtension vK L

theorem

doubleCosetExtension_mk

L149 ↗

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section AbsoluteValueExtensions
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
variable (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK M)
    (L : IntermediateField K M)
local notation "G" => M ≃ₐ[K] M
local notation "H" => L.fixingSubgroup
local notation "D" => absoluteValueDecompositionGroup K w.val

Lean source · statement

theorem doubleCosetExtension_mk
    (g : G) :
    doubleCosetExtension vK hvK w L
        (DoubleCoset.mk H D g) =
      restrictAbsoluteValueExtensionToIntermediate
        vK
        (absoluteValueExtensionConjugate
          vK w g⁻¹)
        L

theorem

doubleCosetExtension_surjective

L162 ↗

Documentation

Every extension of v to the intermediate field occurs by restricting a conjugate of w.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section AbsoluteValueExtensions
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
variable (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK M)
    (L : IntermediateField K M)
local notation "G" => M ≃ₐ[K] M
local notation "H" => L.fixingSubgroup
local notation "D" => absoluteValueDecompositionGroup K w.val

Lean source · statement

theorem doubleCosetExtension_surjective
    [FiniteDimensional K M] [IsGalois K M] :
    Function.Surjective
      (doubleCosetExtension vK hvK w L)

theorem

doubleCosetExtension_injective

L194 ↗

Documentation

Equality after restriction to L is precisely equality of the corresponding double cosets. The proof applies valuation-extension counting over L and then reads the resulting L-automorphism as an element of H = Gal(M / L).

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section AbsoluteValueExtensions
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
variable (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK M)
    (L : IntermediateField K M)
local notation "G" => M ≃ₐ[K] M
local notation "H" => L.fixingSubgroup
local notation "D" => absoluteValueDecompositionGroup K w.val

Lean source · statement

theorem doubleCosetExtension_injective
    [IsGalois K M] :
    Function.Injective
      (doubleCosetExtension vK hvK w L)

def

doubleCosetExtensionEquiv

L296 ↗

Documentation

The place-counting equivalence in the orientation needed for the normal-closure reduction.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section AbsoluteValueExtensions
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
variable (vK : AbsoluteValue K ℝ)
    (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK M)
    (L : IntermediateField K M)
local notation "G" => M ≃ₐ[K] M
local notation "H" => L.fixingSubgroup
local notation "D" => absoluteValueDecompositionGroup K w.val

Lean source · statement

def doubleCosetExtensionEquiv
    [FiniteDimensional K M] [IsGalois K M] :
    DoubleCoset.Quotient (H : Set G) D ≃
      AbsoluteValueExtension vK L

def

AbsoluteValueSplitsCompletelyInExtension

L319 ↗

Documentation

Intrinsic complete splitting for an arbitrary finite extension: the number of actual extensions of the absolute value is the full degree. Unlike a decomposition-group definition, this remains correct when E / K is not Galois.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section CompleteSplitting
variable {K E : Type}
    [Field K] [Field E] [Algebra K E]
    [FiniteDimensional K E]

Lean source · statement

def AbsoluteValueSplitsCompletelyInExtension
    (vK : AbsoluteValue K ℝ) : Prop

def

FinitePlaceSplitsCompletelyInExtension

L328 ↗

Documentation

Intrinsic complete splitting of a finite place in a possibly non-Galois finite extension.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section CompleteSplitting
variable {K E : Type}
    [Field K] [Field E] [Algebra K E]
    [FiniteDimensional K E]
variable [NumberField K]

Lean source · statement

def FinitePlaceSplitsCompletelyInExtension
    (v : HeightOneSpectrum (𝓞 K)) : Prop

theorem

leftCosetDoubleCoset_card_eq_finrank

L346 ↗

Documentation

The left-coset space H \ G = H \ G / 1 has cardinality [L : K] for H = Gal(M / L).

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section DoubleCosetCount
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
    [IsGalois K M]
local notation "G" => M ≃ₐ[K] M

Lean source · statement

theorem leftCosetDoubleCoset_card_eq_finrank
    (L : IntermediateField K M) :
    Nat.card
        (DoubleCoset.Quotient
          (L.fixingSubgroup : Set G)
          (⊥ : Subgroup G)) =
      Module.finrank K L

theorem

absoluteValueSplitsCompletelyInExtension_iff_doubleCoset_card_eq

L382 ↗

Documentation

Place counting plus the definition of complete splitting: v splits completely in L exactly when the double-coset count equals the left-coset count.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section DoubleCosetCount
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
    [IsGalois K M]
local notation "G" => M ≃ₐ[K] M
variable [FiniteDimensional K M]
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK M)
    (L : IntermediateField K M)

Lean source · statement

theorem absoluteValueSplitsCompletelyInExtension_iff_doubleCoset_card_eq
    (hvK : vK.IsNontrivial) :
    AbsoluteValueSplitsCompletelyInExtension
        (E := L) vK ↔
      Nat.card
          (DoubleCoset.Quotient
            (L.fixingSubgroup : Set G)
            (absoluteValueDecompositionGroup K w.1)) =
        Nat.card
          (DoubleCoset.Quotient
            (L.fixingSubgroup : Set G)
            (⊥ : Subgroup G))

theorem

absoluteValueDecompositionGroup_eq_bot_of_splitsCompletelyInIntermediate

L404 ↗

Documentation

The actual decomposition group is trivial as soon as an intermediate field with core-free fixing subgroup is completely split. This is the reusable source-producing form of the normal-closure normal-closure splitting argument.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section DoubleCosetCount
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
    [IsGalois K M]
local notation "G" => M ≃ₐ[K] M
variable [FiniteDimensional K M]
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK M)
    (L : IntermediateField K M)

Lean source · statement

theorem absoluteValueDecompositionGroup_eq_bot_of_splitsCompletelyInIntermediate
    (hvK : vK.IsNontrivial)
    (hcore :
      L.fixingSubgroup.normalCore = ⊥)
    (hsplit :
      AbsoluteValueSplitsCompletelyInExtension
        (E := L) vK) :
    absoluteValueDecompositionGroup K w.1 = ⊥

theorem

absoluteValueDecompositionGroup_eq_bot_of_splitsCompletelyInFixedField

L423 ↗

Documentation

Fixed-field spelling of the preceding source theorem. This is the literal L = M^H formulation used in the normal-closure reduction.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section DoubleCosetCount
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
    [IsGalois K M]
local notation "G" => M ≃ₐ[K] M
variable [FiniteDimensional K M]
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK M)
    (L : IntermediateField K M)

Lean source · statement

theorem absoluteValueDecompositionGroup_eq_bot_of_splitsCompletelyInFixedField
    (hvK : vK.IsNontrivial)
    (H : Subgroup G)
    (hcore : H.normalCore = ⊥)
    (hsplit :
      AbsoluteValueSplitsCompletelyInExtension
        (E := IntermediateField.fixedField H) vK) :
    absoluteValueDecompositionGroup K w.1 = ⊥

theorem

fixingSubgroup_normalCore_eq_bot_of_normalClosure_eq_top

L452 ↗

Documentation

If the conjugates of L generate the ambient Galois extension, then Gal(M / L) is core-free. This derives the group-theoretic normal-closure condition from the actual field-theoretic normal closure, rather than taking it as an additional hypothesis.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section NormalClosure
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]

Lean source · statement

theorem fixingSubgroup_normalCore_eq_bot_of_normalClosure_eq_top
    (L : IntermediateField K M)
    (hclosure :
      IntermediateField.normalClosure K L M = ⊤) :
    L.fixingSubgroup.normalCore = ⊥

theorem

fixingSubgroup_normalCore_eq_bot_of_isNormalClosure

L483 ↗

Documentation

Class-valued normal-closure form of the preceding theorem.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section NormalClosure
variable {K M : Type}
    [Field K] [Field M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]

Lean source · statement

theorem fixingSubgroup_normalCore_eq_bot_of_isNormalClosure
    (L : IntermediateField K M)
    [IsNormalClosure K L M] :
    L.fixingSubgroup.normalCore = ⊥

theorem

finitePlaceSplitsCompletelyInExtension_iff_doubleCoset_card_eq

L508 ↗

Documentation

The double-coset criterion for an actual finite place and the decomposition group attached to the standard chosen extension to M.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FinitePlaces
variable {K M : Type}
    [Field K] [NumberField K]
    [Field M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
local notation "G" => M ≃ₐ[K] M

Lean source · statement

theorem finitePlaceSplitsCompletelyInExtension_iff_doubleCoset_card_eq
    (L : IntermediateField K M)
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePlaceSplitsCompletelyInExtension
        (K := K) (E := L) v ↔
      Nat.card
          (DoubleCoset.Quotient
            (L.fixingSubgroup : Set G)
            (finitePlaceDecompositionGroup
              (K := K) (L := M) v)) =
        Nat.card
          (DoubleCoset.Quotient
            (L.fixingSubgroup : Set G)
            (⊥ : Subgroup G))

theorem

finitePlaceSplitsCompletely_in_ambient_of_fixedField

L531 ↗

Documentation

Literal fixed-field form: if H is core-free and the finite place splits completely in M^H, then it splits completely in M.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FinitePlaces
variable {K M : Type}
    [Field K] [NumberField K]
    [Field M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
local notation "G" => M ≃ₐ[K] M

Lean source · statement

theorem finitePlaceSplitsCompletely_in_ambient_of_fixedField
    (H : Subgroup G)
    (hcore : H.normalCore = ⊥)
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      FinitePlaceSplitsCompletelyInExtension
        (K := K)
        (E := IntermediateField.fixedField H) v) :
    FinitePlaceSplitsCompletely
      (K := K) (L := M) v

theorem

finitePlaceSplitsCompletely_in_normalClosure

L555 ↗

Documentation

Source-producing normal-closure reduction for a finite place.

The hypothesis says that M is generated by the K-conjugates of L. Complete splitting in the possibly non-Galois intermediate extension gives the double-coset cardinality equality, the normal closure makes the fixing subgroup core-free, and the actual chosen decomposition group in M / K is therefore trivial.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FinitePlaces
variable {K M : Type}
    [Field K] [NumberField K]
    [Field M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
local notation "G" => M ≃ₐ[K] M

Lean source · statement

theorem finitePlaceSplitsCompletely_in_normalClosure
    (L : IntermediateField K M)
    (hclosure :
      IntermediateField.normalClosure K L M = ⊤)
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      FinitePlaceSplitsCompletelyInExtension
        (K := K) (E := L) v) :
    FinitePlaceSplitsCompletely
      (K := K) (L := M) v

theorem

finitePlaceSplitsCompletely_in_isNormalClosure

L577 ↗

Documentation

Complete splitting ascends to an ambient field carrying the actual IsNormalClosure instance.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FinitePlaces
variable {K M : Type}
    [Field K] [NumberField K]
    [Field M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
local notation "G" => M ≃ₐ[K] M

Lean source · statement

theorem finitePlaceSplitsCompletely_in_isNormalClosure
    (L : IntermediateField K M)
    [IsNormalClosure K L M]
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      FinitePlaceSplitsCompletelyInExtension
        (K := K) (E := L) v) :
    FinitePlaceSplitsCompletely
      (K := K) (L := M) v

theorem

finitePlace_normalClosure_doubleCoset_source

L597 ↗

Documentation

The same result displayed together with the intermediate double-coset equality that drives the proof.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FinitePlaces
variable {K M : Type}
    [Field K] [NumberField K]
    [Field M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
local notation "G" => M ≃ₐ[K] M

Lean source · statement

theorem finitePlace_normalClosure_doubleCoset_source
    (L : IntermediateField K M)
    (hclosure :
      IntermediateField.normalClosure K L M = ⊤)
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      FinitePlaceSplitsCompletelyInExtension
        (K := K) (E := L) v) :
    (Nat.card
          (DoubleCoset.Quotient
            (L.fixingSubgroup : Set G)
            (finitePlaceDecompositionGroup
              (K := K) (L := M) v)) =
        Nat.card
          (DoubleCoset.Quotient
            (L.fixingSubgroup : Set G)
            (⊥ : Subgroup G))) ∧
      FinitePlaceSplitsCompletely
        (K := K) (L := M) v

def

absoluteValueExtensionEquivOfAlgEquiv

L634 ↗

Documentation

Transport extensions of an absolute value through an algebra equivalence of finite extensions.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section SplittingTransport
variable
    {K E E' : Type}
    [Field K]
    [Field E] [Algebra K E]
    [Field E'] [Algebra K E']

Lean source · full declaration

def absoluteValueExtensionEquivOfAlgEquiv
    (v : AbsoluteValue K ℝ)
    (e : E ≃ₐ[K] E') :
    AbsoluteValueExtension v E ≃
      AbsoluteValueExtension v E' where
  toFun w :=
    { val :=
        w.1.comp (f := e.symm.toRingHom)
          e.symm.injective
      property := by
        intro x
        change w.1 (e.symm (algebraMap K E' x)) = v x
        rw [e.symm.commutes]
        exact w.2 x }
  invFun w :=
    { val :=
        w.1.comp (f := e.toRingHom)
          e.injective
      property := by
        intro x
        change w.1 (e (algebraMap K E x)) = v x
        rw [e.commutes]
        exact w.2 x }
  left_inv w := by
    apply Subtype.ext
    ext x
    change w.1 (e.symm (e x)) = w.1 x
    rw [e.symm_apply_apply]
  right_inv w := by
    apply Subtype.ext
    ext x
    change w.1 (e (e.symm x)) = w.1 x
    rw [e.apply_symm_apply]

theorem

absoluteValueSplitsCompletelyInExtension_algEquiv

L674 ↗

Documentation

Intrinsic complete splitting is invariant under replacing the extension by an isomorphic K-algebra.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section SplittingTransport
variable
    {K E E' : Type}
    [Field K]
    [Field E] [Algebra K E]
    [Field E'] [Algebra K E']
variable [FiniteDimensional K E]
    [FiniteDimensional K E']
omit [FiniteDimensional K E] [FiniteDimensional K E'] in

Lean source · statement

theorem absoluteValueSplitsCompletelyInExtension_algEquiv
    (v : AbsoluteValue K ℝ)
    (e : E ≃ₐ[K] E') :
    AbsoluteValueSplitsCompletelyInExtension
        (E := E) v ↔
      AbsoluteValueSplitsCompletelyInExtension
        (E := E') v

theorem

finitePlaceSplitsCompletelyInExtension_algEquiv

L691 ↗

Documentation

Finite-place complete splitting is invariant under a K-algebra equivalence.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section SplittingTransport
variable
    {K E E' : Type}
    [Field K]
    [Field E] [Algebra K E]
    [Field E'] [Algebra K E']
variable [FiniteDimensional K E]
    [FiniteDimensional K E']
variable [NumberField K]
omit [FiniteDimensional K E] [FiniteDimensional K E'] in

Lean source · statement

theorem finitePlaceSplitsCompletelyInExtension_algEquiv
    (e : E ≃ₐ[K] E')
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePlaceSplitsCompletelyInExtension
        (K := K) (E := E) v ↔
      FinitePlaceSplitsCompletelyInExtension
        (K := K) (E := E') v

theorem

finitePlaceSplitsCompletely_iff_inExtension

L715 ↗

Documentation

For a finite Galois extension, complete splitting defined by the chosen decomposition group is equivalent to intrinsic complete splitting by the number of extensions of the place.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section GaloisSplittingBridge
variable
    {K E : Type}
    [Field K] [NumberField K]
    [Field E] [Algebra K E]
    [FiniteDimensional K E]
    [IsGalois K E]

Lean source · statement

theorem finitePlaceSplitsCompletely_iff_inExtension
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePlaceSplitsCompletely
        (K := K) (L := E) v ↔
      FinitePlaceSplitsCompletelyInExtension
        (K := K) (E := E) v

theorem

finitePlaceSplitsCompletely_of_decompositionGroup_le_restrictNormalHom_ker

L777 ↗

Documentation

If the decomposition group upstairs acts trivially on a normal subextension, then the finite place splits completely in that subextension.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section SplittingThroughRestriction
variable
    {K E N : Type}
    [Field K] [NumberField K]
    [Field E] [Algebra K E]
    [FiniteDimensional K E] [IsGalois K E]
    [Field N] [Algebra K N] [Algebra E N]
    [IsScalarTower K E N]
    [FiniteDimensional K N] [IsGalois K N]
omit [FiniteDimensional K N] in

Lean source · statement

theorem
    finitePlaceSplitsCompletely_of_decompositionGroup_le_restrictNormalHom_ker
    (v : HeightOneSpectrum (𝓞 K))
    (h :
      finitePlaceDecompositionGroup (K := K) (L := N) v ≤
        (AlgEquiv.restrictNormalHom
          (F := K) (K₁ := N) (E := E)).ker) :
    FinitePlaceSplitsCompletely (K := K) (L := E) v

theorem

finiteNormalClosureOriginalField_fixingSubgroup_normalCore

L882 ↗

Documentation

The fixing subgroup of the distinguished copy of L is core-free in the Galois group of its finite normal closure.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FiniteNormalClosure
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem finiteNormalClosureOriginalField_fixingSubgroup_normalCore :
    (finiteNormalClosureOriginalField K L).fixingSubgroup.normalCore =
      ⊥

theorem

finitePlaceSplitsCompletely_in_finiteNormalClosure

L892 ↗

Documentation

Complete splitting in the original extension forces complete splitting in its finite normal closure.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FiniteNormalClosure
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem finitePlaceSplitsCompletely_in_finiteNormalClosure
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      FinitePlaceSplitsCompletelyInExtension
        (K := K)
        (E := finiteNormalClosureOriginalField K L) v) :
    FinitePlaceSplitsCompletely
      (K := K) (L := finiteNormalClosure K L) v

theorem

finite_nonSplittingPlaces_finiteNormalClosure

L908 ↗

Documentation

If only finitely many finite places fail to split completely in L, the same is true in the finite normal closure.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FiniteNormalClosure
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem finite_nonSplittingPlaces_finiteNormalClosure
    (hfinite :
      {v : HeightOneSpectrum (𝓞 K) |
        ¬ FinitePlaceSplitsCompletelyInExtension
          (K := K)
          (E := finiteNormalClosureOriginalField K L) v}.Finite) :
    {v : HeightOneSpectrum (𝓞 K) |
      ¬ FinitePlaceSplitsCompletely
        (K := K) (L := finiteNormalClosure K L) v}.Finite

theorem

finite_nonSplittingPlaces_originalField

L925 ↗

Documentation

Finiteness of the nonsplitting set in the original field transports to its distinguished copy in the finite normal closure.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FiniteNormalClosure
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem finite_nonSplittingPlaces_originalField
    (hfinite :
      {v : HeightOneSpectrum (𝓞 K) |
        ¬ FinitePlaceSplitsCompletelyInExtension
          (K := K) (E := L) v}.Finite) :
    {v : HeightOneSpectrum (𝓞 K) |
      ¬ FinitePlaceSplitsCompletelyInExtension
        (K := K)
        (E := finiteNormalClosureOriginalField K L) v}.Finite

theorem

finite_nonSplittingPlaces_normalClosure_of_original

L940 ↗

Documentation

Finiteness of the nonsplitting set in L / K implies finiteness of the nonsplitting set in its finite normal closure.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FiniteNormalClosure
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem finite_nonSplittingPlaces_normalClosure_of_original
    (hfinite :
      {v : HeightOneSpectrum (𝓞 K) |
        ¬ FinitePlaceSplitsCompletelyInExtension
          (K := K) (E := L) v}.Finite) :
    {v : HeightOneSpectrum (𝓞 K) |
      ¬ FinitePlaceSplitsCompletely
        (K := K) (L := finiteNormalClosure K L) v}.Finite

Module documentation

Complete splitting and normal closures

Declarations