LocalClassFieldTheory.chosenNormalBasisPrincipalUnitLatticeClass_galoisGroup
The class u - 1 in the normal-basis lattice graded piece is equivariant for the actual Galois action on integer units and the transported action on the lattice quotient.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology
noncomputable section
universe u
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]
[ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
[ValuativeRel L]
[Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
[IsIntegralClosure 𝒪[L] 𝒪[K] L]Lean source · full declaration
theorem chosenNormalBasisPrincipalUnitLatticeClass_galoisGroup
(n : Nat) (sigma : Gal(L/K)) (u : 𝒪[L]ˣ)
(hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
letI := galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction K L n
chosenNormalBasisPrincipalUnitLatticeClass K L n (sigma • u)
(galoisGroup_smul_mem_chosenNormalBasisPrincipalUnitSet
(K := K) (L := L) n sigma hu) =
sigma • chosenNormalBasisPrincipalUnitLatticeClass K L n u hu := by
let := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
let := galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction K L n
let y : chosenBaseUniformizerPowSubmodule K L n
(chosenNormalBasisIntegerLattice K L) :=
⟨((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L), hu⟩
let x : chosenNormalBasisIntegerLattice K L :=
(chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n).symm y
have hxy : chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n x = y :=
(chosenNormalBasisIntegerLatticeMulPowLinearEquiv K L n).apply_symm_apply y
rw [chosenNormalBasisPrincipalUnitLatticeClass,
chosenNormalBasisPrincipalUnitLatticeClass]
change chosenNormalBasisLatticeSuccQuotMk K L n _ =
sigma • chosenNormalBasisLatticeSuccQuotMk K L n y
rw [← hxy,
galoisGroupChosenNormalBasisLatticeSuccQuotDistribMulAction_smul_mk_mulPow]
apply congrArg (chosenNormalBasisLatticeSuccQuotMk K L n)
apply Subtype.ext
have hfield := chosenNormalBasisIntegerLatticeMulPowLinearEquiv_galoisGroup_apply_coe
K L n sigma x
rw [hxy] at hfield
simpa [y, galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure_smul,
map_sub, map_one] using hfield.symm