Module

FiniteLevelIntersections.lean

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.FiniteLevelIntersections

10 declarations indexed from sourceView source ↗

Module documentation

Finite-level ramification intersections for a complete discretely valued field

At each finite Galois level, this file uses the chosen integral-closure valuation from FiniteGaloisLevel and intersects the inverse images of its ramification groups. Independence from the chosen complete-DVF realization is proved in FiniteGaloisLevelIndependence. Finite-quotient compatibility has not been proved, so neither intersection is identified with a canonical absolute ramification filtration.

Imports2

Imported by1

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.All

def

finiteLevelUpperIntersection

L36 ↗

RamificationTheory.Field.absoluteGaloisGroup.finiteLevelUpperIntersection

Documentation

The raw intersection of the inverse images of the chosen upper ramification groups over all finite Galois levels. Choice-independence is proved by the companion FiniteGaloisLevelIndependence module; no finite-quotient compatibility is asserted here.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

def finiteLevelUpperIntersection
    (base : CompleteDVF.{u, v} K) (t : ℝ) :
    Subgroup (Field.absoluteGaloisGroup K)

theorem

mem_finiteLevelUpperIntersection_iff

L47 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_finiteLevelUpperIntersection_iff

Documentation

States the theorem mem_finiteLevelUpperIntersection_iff.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

theorem mem_finiteLevelUpperIntersection_iff
    (base : CompleteDVF.{u, v} K) (t : ℝ)
    (sigma : Field.absoluteGaloisGroup K) :
    sigma ∈ finiteLevelUpperIntersection K base t ↔
      ∀ E : FiniteGaloisIntermediateField K (AlgebraicClosure K),
        AlgEquiv.restrictNormalHom (F := K) (K₁ := AlgebraicClosure K)
          E.toIntermediateField sigma ∈
          HilbertRamification.FiniteGaloisLevel.chosenUpperRamificationGroup
            base E t

def

finiteLevelLowerIntersection

L66 ↗

RamificationTheory.Field.absoluteGaloisGroup.finiteLevelLowerIntersection

Documentation

The raw same-index intersection of the integral lower groups at all finite Galois levels. This is not presented as a canonical absolute lower numbering: lower numbering is not quotient-compatible in the way upper numbering is.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

def finiteLevelLowerIntersection
    (base : CompleteDVF.{u, v} K) (n : ℕ) :
    Subgroup (Field.absoluteGaloisGroup K)

theorem

mem_finiteLevelLowerIntersection_iff

L78 ↗

RamificationTheory.Field.absoluteGaloisGroup.mem_finiteLevelLowerIntersection_iff

Documentation

States the theorem mem_finiteLevelLowerIntersection_iff.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

theorem mem_finiteLevelLowerIntersection_iff
    (base : CompleteDVF.{u, v} K) (n : ℕ)
    (sigma : Field.absoluteGaloisGroup K) :
    sigma ∈ finiteLevelLowerIntersection K base n ↔
      ∀ E : FiniteGaloisIntermediateField K (AlgebraicClosure K),
        AlgEquiv.restrictNormalHom (F := K) (K₁ := AlgebraicClosure K)
          E.toIntermediateField sigma ∈
          (HilbertRamification.FiniteGaloisLevel.chosenLowerRamificationFiltration
            base E).lower n

theorem

finiteLevelUpperIntersection_normal

L95 ↗

RamificationTheory.Field.absoluteGaloisGroup.finiteLevelUpperIntersection_normal

Documentation

States the theorem finiteLevelUpperIntersection_normal.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

theorem finiteLevelUpperIntersection_normal
    (base : CompleteDVF.{u, v} K) (t : ℝ) :
    (finiteLevelUpperIntersection K base t).Normal

theorem

finiteLevelLowerIntersection_normal

L107 ↗

RamificationTheory.Field.absoluteGaloisGroup.finiteLevelLowerIntersection_normal

Documentation

States the theorem finiteLevelLowerIntersection_normal.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

theorem finiteLevelLowerIntersection_normal
    (base : CompleteDVF.{u, v} K) (n : ℕ) :
    (finiteLevelLowerIntersection K base n).Normal

theorem

finiteLevelUpperComap_isClosed

L120 ↗

RamificationTheory.Field.absoluteGaloisGroup.finiteLevelUpperComap_isClosed

Documentation

A finite-level upper group has closed inverse image in the absolute Galois group.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

theorem finiteLevelUpperComap_isClosed
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (t : ℝ) :
    IsClosed
      (Subgroup.comap
        (AlgEquiv.restrictNormalHom (F := K) (K₁ := AlgebraicClosure K)
          E.toIntermediateField)
        (HilbertRamification.FiniteGaloisLevel.chosenUpperRamificationGroup
          base E t)).carrier

theorem

finiteLevelLowerComap_isClosed

L142 ↗

RamificationTheory.Field.absoluteGaloisGroup.finiteLevelLowerComap_isClosed

Documentation

A finite-level integral lower group has closed inverse image in the absolute Galois group.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

theorem finiteLevelLowerComap_isClosed
    (base : CompleteDVF.{u, v} K)
    (E : FiniteGaloisIntermediateField K (AlgebraicClosure K))
    (n : ℕ) :
    IsClosed
      (Subgroup.comap
        (AlgEquiv.restrictNormalHom (F := K) (K₁ := AlgebraicClosure K)
          E.toIntermediateField)
        ((HilbertRamification.FiniteGaloisLevel.chosenLowerRamificationFiltration
          base E).lower n)).carrier

theorem

finiteLevelUpperIntersection_isClosed

L163 ↗

RamificationTheory.Field.absoluteGaloisGroup.finiteLevelUpperIntersection_isClosed

Documentation

The finite-level upper intersection is closed.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

theorem finiteLevelUpperIntersection_isClosed
    (base : CompleteDVF.{u, v} K) (t : ℝ) :
    IsClosed
      (finiteLevelUpperIntersection K base t :
        Set (Field.absoluteGaloisGroup K))

theorem

finiteLevelLowerIntersection_isClosed

L172 ↗

RamificationTheory.Field.absoluteGaloisGroup.finiteLevelLowerIntersection_isClosed

Documentation

The finite-level lower intersection is closed.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.Field.absoluteGaloisGroup
open ValuationTheory.DiscreteValuationField
variable (K : Type u) [Field K]

Lean source · statement

theorem finiteLevelLowerIntersection_isClosed
    (base : CompleteDVF.{u, v} K) (n : ℕ) :
    IsClosed
      (finiteLevelLowerIntersection K base n :
        Set (Field.absoluteGaloisGroup K))

Module documentation

Finite-level ramification intersections for a complete discretely valued field

Declarations