MathlibNormInterface.lean

theorem isFieldNorm_iff_mem_globalFieldNormSubgroup
    (K L : Type)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    (x : Kˣ) :
    ClassFieldTheory.IsFieldNorm K L x ↔
      x ∈ GlobalClassFieldTheory.ClassFieldAxiom.globalFieldNormSubgroup K L

theorem isNormAtFinitePlace_iff
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (w : HeightOneSpectrum (𝓞 K)) (x : Kˣ) :
    ClassFieldTheory.IsNormAtFinitePlace K L w x ↔
      IdeleGroup.finiteComponent w (IdeleGroup.principalIdele K x) ∈
        chosenFinitePlaceLocalNormSubgroup (K := K) (L := L) w

theorem isNormAtInfinitePlace_iff
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
    (w : InfinitePlace K) (x : Kˣ) :
    ClassFieldTheory.IsNormAtInfinitePlace K L w x ↔
      IdeleGroup.infiniteComponent w (IdeleGroup.principalIdele K x) ∈
        (Units.map
          (Algebra.norm w.Completion :
            (w.Completion ⊗[K] L) →* w.Completion)).range

theorem isEverywhereLocalNorm_iff_mem_everywhereLocalFieldNormSubgroup
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (x : Kˣ) :
    ClassFieldTheory.IsEverywhereLocalNorm K L x ↔
      x ∈ GlobalClassFieldTheory.ClassFieldAxiom.everywhereLocalFieldNormSubgroup K L

theorem norm_includeRight
    (K L A : Type)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    [CommRing A] [Algebra K A] [Nontrivial A]
    (y : L) :
    Algebra.norm A
        (Algebra.TensorProduct.includeRight (R := K) (A := A) (B := L) y) =
      algebraMap K A (Algebra.norm K y)

theorem globalNorm_isEverywhereLocalNorm
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
    (x : Kˣ) :
    ClassFieldTheory.IsFieldNorm K L x →
      ClassFieldTheory.IsEverywhereLocalNorm K L x

theorem cyclicHasseNormTheorem
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
    (x : Kˣ) :
    ClassFieldTheory.IsFieldNorm K L x ↔
      ClassFieldTheory.IsEverywhereLocalNorm K L x