Module

NormContainment.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.IdeleClassPowerLocalUnitQuotient.NormContainment

2 declarations indexed from sourceView source ↗

Module documentation

Norm containment for idele power-local-unit subgroups

This file proves that the concrete local-condition subgroup lies in the global idele norm range, and descends that inclusion to idele classes.

Imports16

Imported by6

theorem

idelePowerLocalUnitSubgroup_le_relativeIdeleNorm_range

L49 ↗

GlobalClassFieldTheory.ClassFieldAxiom.idelePowerLocalUnitSubgroup_le_relativeIdeleNorm_range

Documentation

The idele norm inclusion h(S,T) ⊆ N_{L/K} I_L.

Source context 10 commands

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

open scoped NumberField NNReal ValuativeRel TensorProduct
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
open scoped Classical in

Lean source · statement

theorem idelePowerLocalUnitSubgroup_le_relativeIdeleNorm_range
    (n : ℕ+) (r : ℕ)
    (eG :
      (L ≃ₐ[K] L) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (harch :
      Even (n : ℕ) ∨
        ∀ w : InfinitePlace K, ¬ w.IsReal)
    (hT :
      ∀ v, v ∈ T →
        _root_.FinitePlaceSplitsCompletely
          (K := K) (L := L) v)
    (hAway :
      ∀ v, v ∉ S ∪ T →
        _root_.ChosenFinitePlaceIsUnramified
          (K := K) (L := L) v) :
    idelePowerLocalUnitSubgroup (K := K) n S T ≤
      (RelativeIdeleGroup.norm K L).range

theorem

ideleClassPowerLocalUnitSubgroup_le_ideleClassNorm_range

L93 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ideleClassPowerLocalUnitSubgroup_le_ideleClassNorm_range