Core.lean

def artinPrincipalUnitGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (n : ℕ) : Subgroup (Gal(L / K))

theorem artinPrincipalUnitGroup_antitone
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    {m n : ℕ} (hmn : m ≤ n) :
    artinPrincipalUnitGroup K L n ≤ artinPrincipalUnitGroup K L m

theorem artinPrincipalUnitGroup_eq_bot_iff
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (n : ℕ) :
    artinPrincipalUnitGroup K L n = ⊥ ↔
      localConductorExponent K L ≤ n

theorem artinPrincipalUnitGroup_ne_bot_iff
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (n : ℕ) :
    artinPrincipalUnitGroup K L n ≠ ⊥ ↔
      n < localConductorExponent K L

theorem artinPrincipalUnitGroup_map_intermediateFieldRestrict
    (K : Type) [Field K]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsAbelianGalois K E] [IsAbelianGalois K F]
    (n : ℕ) :
    Subgroup.map
        (intermediateFieldRestrictNormalHom E F hEF)
        (artinPrincipalUnitGroup K F n) =
      artinPrincipalUnitGroup K E n

def artinPrincipalUnitStepGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (t : ℝ) : Subgroup (Gal(L / K))

theorem artinPrincipalUnitStepGroup_map_intermediateFieldRestrict
    (K : Type) [Field K]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsAbelianGalois K E] [IsAbelianGalois K F]
    (t : ℝ) :
    Subgroup.map
        (intermediateFieldRestrictNormalHom E F hEF)
        (artinPrincipalUnitStepGroup K F t) =
      artinPrincipalUnitStepGroup K E t

theorem filteredLocalReciprocity_descends
    (K : Type) [Field K]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsAbelianGalois K E] [IsAbelianGalois K F]
    (upperE : ℝ → Subgroup (Gal(E/K)))
    (upperF : ℝ → Subgroup (Gal(F/K)))
    (hupper : ∀ t,
      Subgroup.map
          (intermediateFieldRestrictNormalHom E F hEF)
          (upperF t) =
        upperE t)
    (hcover : ∀ t, 0 ≤ t →
      artinPrincipalUnitStepGroup K F t = upperF t)
    (t : ℝ) (ht : 0 ≤ t) :
    artinPrincipalUnitStepGroup K E t = upperE t

def IsArtinPrincipalUnitJump
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (t : ℝ) : Prop

theorem isArtinPrincipalUnitJump_natCast_iff
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (n : ℕ) :
    IsArtinPrincipalUnitJump K L (n : ℝ) ↔
      artinPrincipalUnitGroup K L n ≠
        artinPrincipalUnitGroup K L (n + 1)

theorem isArtinPrincipalUnitJump_integer
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    {t : ℝ} (ht : IsArtinPrincipalUnitJump K L t) :
    ∃ n : ℕ, t = n

theorem exists_lastArtinPrincipalUnitJump_of_conductor_pos
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (hcond : 0 < localConductorExponent K L) :
    ∃ n : ℕ,
      localConductorExponent K L = n + 1 ∧
        IsArtinPrincipalUnitJump K L (n : ℝ)