LocalClassFieldTheory.exists_localIntegerUnitsHerbrandDefinedAndEqOne
The integer-unit Herbrand witness used by the local class-field axiom, including the proof that its Herbrand quotient is one.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]
[ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
[ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
[IsNonarchimedeanLocalField L]
[Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
[IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]Lean source · full declaration
theorem exists_localIntegerUnitsHerbrandDefinedAndEqOne
(g : Gal(L/K))
(hg : ∀ sigma : Gal(L / K), sigma ∈ Subgroup.zpowers g) :
letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
∃ hU : HerbrandQuotientDefined (Gal(L / K)) 𝒪[L]ˣ g,
@herbrandQuotient (Gal(L / K)) 𝒪[L]ˣ _ _ _
(galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L)
g hU.1 hU.2 = 1 := by
rcases exists_chosenNormalBasisPrincipalUnitSubgroup
(K := K) (L := L) with ⟨cV, hcV⟩
rcases exists_chosenNormalBasisPrincipalUnit_herbrand_subsingleton
(K := K) (L := L) g hg with ⟨cH, hcH⟩
rcases exists_integerUnits_herbrandQuotient_eq_one_of_large_chosenNormalBasisLevel
(K := K) (L := L) with ⟨cU, hcU⟩
let n : Nat := max cV (max cH cU)
have hcVn : cV ≤ n := le_max_left cV (max cH cU)
have hrest : max cH cU ≤ n := le_max_right cV (max cH cU)
have hcHn : cH ≤ n := le_trans (le_max_left cH cU) hrest
have hcUn : cU ≤ n := le_trans (le_max_right cH cU) hrest
rcases hcV n hcVn with ⟨V, hV, _hVprincipal⟩
let := chosenNormalBasisPrincipalUnitSubgroupMulDistribMulAction
K L n V hV
let := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
let := chosenNormalBasisIntegerUnitsQuotMulDistribMulAction K L n V hV
have hcoh := hcH n hcHn V hV
rcases hcU n hcUn V hV g hg hcoh.1 hcoh.2 with ⟨hU, hUone⟩
exact ⟨hU, hUone⟩