NYLL
Module

Decomposition.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.Decomposition
22 declarations indexed from sourceView source ↗

Module documentation

Finite-support decompositions of actual ideles

For a finite set S of finite places, this file identifies the actual subgroup I_K^S with the product of all archimedean local groups, the full multiplicative groups at places in S, and the local unit groups away from S. The construction is componentwise and uses the genuine restricted-product membership condition.

For a finite family of base places in a Galois extension, it also assembles the local tensor-algebra decomposition and proves its equivariance for the full Galois action. Finally, the concrete unramified local class-field theorem is transported through Shapiro to show that every unramified induced integer-unit block has trivial H⁰ and H⁻¹.

Imports15
Imported by4

Declarations

abbrev

FiniteSPlaceFactors

L62 ↗
Documentation

The finite local factors occurring in I_F^S: arbitrary local elements on S, and integral local units away from S.

Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · statement
abbrev FiniteSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 F)))
abbrev

IdeleSPlaceFactors

L71 ↗
Documentation

The complete product model for I_F^S, including every archimedean component.

Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · statement
abbrev IdeleSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 F)))
def

finiteIdeleOfSPlaceFactors

L78 ↗
Documentation

Assemble prescribed local factors into a finite idele. Restricted product membership follows because the only possibly nonintegral components lie in the finite set S.

Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · statement
def finiteIdeleOfSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 F)))
    (x : FiniteSPlaceFactors (F := F) S) :
    FiniteIdeleGroup F
theorem

finiteIdeleOfSPlaceFactors_apply_mem

L96 ↗
Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · statement
theorem finiteIdeleOfSPlaceFactors_apply_mem
    (S : Finset (HeightOneSpectrum (𝓞 F)))
    (x : FiniteSPlaceFactors (F := F) S)
    (v : HeightOneSpectrum (𝓞 F)) (hv : v ∈ S) :
    finiteIdeleOfSPlaceFactors S x v = x.1 ⟨v, hv⟩
theorem

finiteIdeleOfSPlaceFactors_apply_notMem

L104 ↗
Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · statement
theorem finiteIdeleOfSPlaceFactors_apply_notMem
    (S : Finset (HeightOneSpectrum (𝓞 F)))
    (x : FiniteSPlaceFactors (F := F) S)
    (v : HeightOneSpectrum (𝓞 F)) (hv : v ∉ S) :
    finiteIdeleOfSPlaceFactors S x v =
      (x.2 ⟨v, hv⟩ : (v.adicCompletion F)ˣ)
def

finiteSupportedAtEquivSPlaceFactors

L114 ↗
Documentation

The finite part of the actual S-idele group is exactly the displayed product of local multiplicative groups and local unit groups.

Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · full declaration
def finiteSupportedAtEquivSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 F))) :
    FiniteIdeleGroup.supportedAt (K := F) (S : Set _) ≃*
      FiniteSPlaceFactors (F := F) S where
  toFun a :=
    ⟨fun v ↦ a.1 v.1,
      fun v ↦ ⟨a.1 v.1, a.2 v.1 v.2⟩⟩
  invFun x :=
    ⟨finiteIdeleOfSPlaceFactors S x, by
      intro v hv
      rw [finiteIdeleOfSPlaceFactors_apply_notMem S x v hv]
      exact (x.2 ⟨v, hv⟩).2⟩
  left_inv a := by
    apply Subtype.ext
    ext v
    by_cases hv : v ∈ S
    · simp [finiteIdeleOfSPlaceFactors_apply_mem, hv]
    · simp [finiteIdeleOfSPlaceFactors_apply_notMem, hv]
  right_inv x := by
    apply Prod.ext
    · funext v
      exact finiteIdeleOfSPlaceFactors_apply_mem S x v.1 v.2
    · funext v
      apply Subtype.ext
      exact finiteIdeleOfSPlaceFactors_apply_notMem S x v.1 v.2
  map_mul' a b := by
    apply Prod.ext
    · funext v
      rfl
    · funext v
      apply Subtype.ext
      rfl
def

ideleSupportedAtEquivInfiniteProd

L152 ↗
Documentation

The actual finite-support decomposition:

I_F^S ≃ I_{F,∞} × (∏_{v∈S} F_vˣ) × (∏_{v∉S} O_vˣ).

Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · full declaration
def ideleSupportedAtEquivInfiniteProd
    (S : Finset (HeightOneSpectrum (𝓞 F))) :
    IdeleGroup.supportedAt (K := F) (S : Set _) ≃*
      InfiniteIdeleGroup F ×
        FiniteIdeleGroup.supportedAt (K := F) (S : Set _) where
  toFun a := ⟨a.1.1, ⟨a.1.2, a.2⟩⟩
  invFun x := ⟨⟨x.1, x.2.1⟩, x.2.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
def

ideleSupportedAtEquivSPlaceFactors

L165 ↗
Documentation

The actual S-idele group identified with its complete family of archimedean, unrestricted finite, and integral finite local factors.

Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · statement
def ideleSupportedAtEquivSPlaceFactors
    (S : Finset (HeightOneSpectrum (𝓞 F))) :
    IdeleGroup.supportedAt (K := F) (S : Set _) ≃*
      IdeleSPlaceFactors (F := F) S
theorem

ideleSupportedAtEquivSPlaceFactors_infinite

L174 ↗
Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · statement
theorem ideleSupportedAtEquivSPlaceFactors_infinite
    (S : Finset (HeightOneSpectrum (𝓞 F)))
    (a : IdeleGroup.supportedAt (K := F) (S : Set _)) :
    (ideleSupportedAtEquivSPlaceFactors S a).1 = a.1.1
theorem

ideleSupportedAtEquivSPlaceFactors_inside

L181 ↗
Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · statement
theorem ideleSupportedAtEquivSPlaceFactors_inside
    (S : Finset (HeightOneSpectrum (𝓞 F)))
    (a : IdeleGroup.supportedAt (K := F) (S : Set _))
    (v : {v : HeightOneSpectrum (𝓞 F) // v ∈ S}) :
    (ideleSupportedAtEquivSPlaceFactors S a).2.1 v =
      a.1.2 v.1
theorem

ideleSupportedAtEquivSPlaceFactors_outside_coe

L190 ↗
Source context 12 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
Lean source · statement
theorem ideleSupportedAtEquivSPlaceFactors_outside_coe
    (S : Finset (HeightOneSpectrum (𝓞 F)))
    (a : IdeleGroup.supportedAt (K := F) (S : Set _))
    (v : {v : HeightOneSpectrum (𝓞 F) // v ∉ S}) :
    ((ideleSupportedAtEquivSPlaceFactors S a).2.2 v :
        (v.1.adicCompletion F)ˣ) =
      a.1.2 v.1
abbrev

LocalTensorFamily

L209 ↗
Documentation

The actual scalar-extended local tensor factors over a family of base places.

Source context 15 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section FiniteTensorFamily
universe uK uL uι
variable {K : Type uK} {L : Type uL}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
abbrev LocalTensorFamily {ι : Type uι}
    (d : ι → LocalPlaceDatum K L)
def

localTensorFamilyAction

L216 ↗
Documentation

The componentwise natural Galois action on a family of local tensor factors.

Source context 15 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section FiniteTensorFamily
universe uK uL uι
variable {K : Type uK} {L : Type uL}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def localTensorFamilyAction {ι : Type uι}
    (d : ι → LocalPlaceDatum K L) :
    MulDistribMulAction (L ≃ₐ[K] L)
      (LocalTensorFamily d)
def

localBlockFamilyAction

L228 ↗
Documentation

The componentwise induced-module action on a local block family.

Source context 15 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section FiniteTensorFamily
universe uK uL uι
variable {K : Type uK} {L : Type uL}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def localBlockFamilyAction {ι : Type uι}
    (d : ι → LocalPlaceDatum K L) :
    MulDistribMulAction (L ≃ₐ[K] L)
      (LocalBlockFamily d)
def

localTensorFamilyEquivLocalBlockFamily

L253 ↗
Documentation

The componentwise local tensor equivalence realizes a finite (or arbitrary) family of actual local tensor unit groups as the corresponding family of induced local blocks.

Source context 15 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section FiniteTensorFamily
universe uK uL uι
variable {K : Type uK} {L : Type uL}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def localTensorFamilyEquivLocalBlockFamily
    {ι : Type uι} (d : ι → LocalPlaceDatum K L) :
    LocalTensorFamily d ≃* LocalBlockFamily d
theorem

localTensorFamilyEquivLocalBlockFamily_smul

L280 ↗
Documentation

The family realization is equivariant for the full Galois action, not merely componentwise multiplicative.

Source context 15 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section FiniteTensorFamily
universe uK uL uι
variable {K : Type uK} {L : Type uL}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem localTensorFamilyEquivLocalBlockFamily_smul
    {ι : Type uι} (d : ι → LocalPlaceDatum K L)
    (τ : L ≃ₐ[K] L) (z : LocalTensorFamily d) :
    localTensorFamilyEquivLocalBlockFamily d
        ((localTensorFamilyAction d).smul τ z) =
      (localBlockFamilyAction d).smul τ
        (localTensorFamilyEquivLocalBlockFamily d z)
theorem

localTensorFamilyEquivLocalBlockFamily_symm_smul

L329 ↗
Documentation

Equivariance of the inverse family realization. This is often the convenient direction when local induced blocks have already been constructed.

Source context 15 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section FiniteTensorFamily
universe uK uL uι
variable {K : Type uK} {L : Type uL}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem localTensorFamilyEquivLocalBlockFamily_symm_smul
    {ι : Type uι} (d : ι → LocalPlaceDatum K L)
    (τ : L ≃ₐ[K] L) (z : LocalBlockFamily d) :
    (localTensorFamilyEquivLocalBlockFamily d).symm
        ((localBlockFamilyAction d).smul τ z) =
      (localTensorFamilyAction d).smul τ
        ((localTensorFamilyEquivLocalBlockFamily d).symm z)
theorem

unramifiedLocalIntegerUnitsHerbrand_subsingleton

L348 ↗
Documentation

Outside the ramified support, the local integer-unit factor has trivial low-degree Tate cohomology. This generator-explicit form is the one needed after restricting a global cyclic generator to a decomposition group.

Source context 13 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section UnramifiedLocalUnits
Lean source · full declaration
theorem unramifiedLocalIntegerUnitsHerbrand_subsingleton
    (k ell : Type)
    [Field k] [Field ell] [Algebra k ell]
    [FiniteDimensional k ell] [IsGalois k ell]
    [ValuativeRel k] [TopologicalSpace k]
    [IsNonarchimedeanLocalField k]
    [ValuativeRel ell] [UniformSpace ell]
    [IsUniformAddGroup ell]
    [IsNonarchimedeanLocalField ell]
    [Valuation.HasExtension
      (ValuativeRel.valuation k) (ValuativeRel.valuation ell)]
    [IsIntegralClosure 𝒪[ell] 𝒪[k] ell]
    [Module.Finite 𝒪[k] 𝒪[ell]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension
      k ell]
    (g : Gal(ell/k))
    (hg : ∀ σ : Gal(ell / k),
      σ ∈ Subgroup.zpowers g) :
    letI :=
      galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure
        k ell
    Subsingleton
        (HerbrandH0 (Gal(ell / k)) 𝒪[ell]ˣ) ∧
      Subsingleton
        (HerbrandHMinusOne
          (Gal(ell / k)) 𝒪[ell]ˣ g) := by
  exact
    (unramified_units_tateCohomology_and_norm_surjective_for_generator
      k ell g hg).1
theorem

unramifiedLocalIntegerUnitsHerbrand_subsingleton_frobenius

L379 ↗
Documentation

Canonical Frobenius form of the same outside-S vanishing.

Source context 13 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section UnramifiedLocalUnits
Lean source · full declaration
theorem unramifiedLocalIntegerUnitsHerbrand_subsingleton_frobenius
    (k ell : Type)
    [Field k] [Field ell] [Algebra k ell]
    [FiniteDimensional k ell] [IsGalois k ell]
    [ValuativeRel k] [TopologicalSpace k]
    [IsNonarchimedeanLocalField k]
    [ValuativeRel ell] [UniformSpace ell]
    [IsUniformAddGroup ell]
    [IsNonarchimedeanLocalField ell]
    [Valuation.HasExtension
      (ValuativeRel.valuation k) (ValuativeRel.valuation ell)]
    [IsIntegralClosure 𝒪[ell] 𝒪[k] ell]
    [Module.Finite 𝒪[k] 𝒪[ell]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension
      k ell] :
    let φ := arithmeticFrobeniusOfUnramifiedValuation k ell
    letI :=
      galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure
        k ell
    Subsingleton
        (HerbrandH0 (Gal(ell / k)) 𝒪[ell]ˣ) ∧
      Subsingleton
        (HerbrandHMinusOne
          (Gal(ell / k)) 𝒪[ell]ˣ φ) := by
  exact
    (unramified_units_tateCohomology_and_norm_surjective
      k ell).1
def

unramifiedInducedIntegerUnitsHerbrandH0Equiv

L416 ↗
Documentation

Shapiro plus change of group identifies an induced unramified integer-unit block with its actual local Galois cohomology in degree zero.

Source context 16 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section UnramifiedLocalUnits
section InducedOutsideSBlock
universe uG
variable {G : Type uG} [Group G] [Fintype G]
Lean source · full declaration
def unramifiedInducedIntegerUnitsHerbrandH0Equiv
    (H : Subgroup G)
    (k ell : Type)
    [Field k] [Field ell] [Algebra k ell]
    [FiniteDimensional k ell]
    [ValuativeRel ell]
    [MulDistribMulAction (Gal(ell/k)) 𝒪[ell]ˣ]
    (e : H ≃* Gal(ell/k))
    (σ : G)
    (hσ : ∀ τ : G, τ ∈ Subgroup.zpowers σ) :
    letI : MulDistribMulAction H 𝒪[ell]ˣ :=
      MulDistribMulAction.compHom 𝒪[ell]ˣ e.toMonoidHom
    letI : Fintype H := Fintype.ofFinite H
    HerbrandH0 G (InducedModule (B := 𝒪[ell]ˣ) H) ≃*
      HerbrandH0 (Gal(ell / k)) 𝒪[ell]ˣ := by
  letI : MulDistribMulAction H 𝒪[ell]ˣ :=
    MulDistribMulAction.compHom 𝒪[ell]ˣ e.toMonoidHom
  letI : Fintype H := Fintype.ofFinite H
  exact
    (inducedHerbrandH0EquivOfFiniteCyclic H σ hσ).trans
      (herbrandH0CompMulEquiv (A := 𝒪[ell]ˣ) e)
def

unramifiedInducedIntegerUnitsHerbrandHMinusOneEquiv

L440 ↗
Documentation

The corresponding Shapiro and change-of-group equivalence in degree minus one.

Source context 16 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section UnramifiedLocalUnits
section InducedOutsideSBlock
universe uG
variable {G : Type uG} [Group G] [Fintype G]
Lean source · full declaration
def unramifiedInducedIntegerUnitsHerbrandHMinusOneEquiv
    (H : Subgroup G)
    (k ell : Type)
    [Field k] [Field ell] [Algebra k ell]
    [FiniteDimensional k ell]
    [ValuativeRel ell]
    [MulDistribMulAction (Gal(ell/k)) 𝒪[ell]ˣ]
    (e : H ≃* Gal(ell/k))
    (σ : G)
    (hσ : ∀ τ : G, τ ∈ Subgroup.zpowers σ) :
    letI : MulDistribMulAction H 𝒪[ell]ˣ :=
      MulDistribMulAction.compHom 𝒪[ell]ˣ e.toMonoidHom
    letI : Fintype H := Fintype.ofFinite H
    HerbrandHMinusOne G
        (InducedModule (B := 𝒪[ell]ˣ) H) σ ≃*
      HerbrandHMinusOne (Gal(ell / k)) 𝒪[ell]ˣ
        (e (subgroupGeneratorOfGenerator H σ hσ)) := by
  letI : MulDistribMulAction H 𝒪[ell]ˣ :=
    MulDistribMulAction.compHom 𝒪[ell]ˣ e.toMonoidHom
  letI : Fintype H := Fintype.ofFinite H
  exact
    (inducedHerbrandHMinusOneEquivOfFiniteCyclic
      H σ hσ).trans
      (herbrandHMinusOneCompMulEquiv
        (A := 𝒪[ell]ˣ) e
        (subgroupGeneratorOfGenerator H σ hσ))
theorem

unramifiedInducedIntegerUnitsHerbrand_subsingleton

L469 ↗
Documentation

An unramified outside-S induced unit block contributes neither degree-zero nor degree-minus-one Tate cohomology.

Source context 16 commands

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

open scoped NumberField RestrictedProduct ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u
variable {F : Type u} [Field F] [NumberField F]
section UnramifiedLocalUnits
section InducedOutsideSBlock
universe uG
variable {G : Type uG} [Group G] [Fintype G]
Lean source · full declaration
theorem unramifiedInducedIntegerUnitsHerbrand_subsingleton
    (H : Subgroup G)
    (k ell : Type)
    [Field k] [Field ell] [Algebra k ell]
    [FiniteDimensional k ell] [IsGalois k ell]
    [ValuativeRel k] [TopologicalSpace k]
    [IsNonarchimedeanLocalField k]
    [ValuativeRel ell] [UniformSpace ell]
    [IsUniformAddGroup ell]
    [IsNonarchimedeanLocalField ell]
    [Valuation.HasExtension
      (ValuativeRel.valuation k) (ValuativeRel.valuation ell)]
    [IsIntegralClosure 𝒪[ell] 𝒪[k] ell]
    [Module.Finite 𝒪[k] 𝒪[ell]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension
      k ell]
    (e : H ≃* Gal(ell/k))
    (σ : G)
    (hσ : ∀ τ : G, τ ∈ Subgroup.zpowers σ) :
    letI : MulDistribMulAction (Gal(ell / k)) 𝒪[ell]ˣ :=
      galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure
        k ell
    letI : MulDistribMulAction H 𝒪[ell]ˣ :=
      MulDistribMulAction.compHom 𝒪[ell]ˣ e.toMonoidHom
    letI : Fintype H := Fintype.ofFinite H
    Subsingleton
        (HerbrandH0 G
          (InducedModule (B := 𝒪[ell]ˣ) H)) ∧
      Subsingleton
        (HerbrandHMinusOne G
          (InducedModule (B := 𝒪[ell]ˣ) H) σ) := by
  let _ : MulDistribMulAction (Gal(ell / k)) 𝒪[ell]ˣ :=
    galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure
      k ell
  let _ : MulDistribMulAction H 𝒪[ell]ˣ :=
    MulDistribMulAction.compHom 𝒪[ell]ˣ e.toMonoidHom
  let _ : Fintype H := Fintype.ofFinite H
  let δ := subgroupGeneratorOfGenerator H σ hσ
  have hδ : ∀ τ : Gal(ell / k),
      τ ∈ Subgroup.zpowers (e δ) := by
    intro τ
    have hmem :
        e.symm τ ∈ Subgroup.zpowers δ :=
      subgroupGeneratorOfGenerator_generates H σ hσ (e.symm τ)
    have himage :
        e (e.symm τ) ∈
          (Subgroup.zpowers δ).map e.toMonoidHom :=
      ⟨e.symm τ, hmem, rfl⟩
    rw [MonoidHom.map_zpowers] at himage
    simpa using himage
  have hlocal :=
    unramifiedLocalIntegerUnitsHerbrand_subsingleton
      k ell (e δ) hδ
  constructor
  · let E :=
      unramifiedInducedIntegerUnitsHerbrandH0Equiv
        H k ell e σ hσ
    exact
      ⟨fun x y ↦ E.injective
        (by exact @Subsingleton.elim _ hlocal.1 (E x) (E y))⟩
  · let E :=
      unramifiedInducedIntegerUnitsHerbrandHMinusOneEquiv
        H k ell e σ hσ
    exact
      ⟨fun x y ↦ E.injective
        (by exact @Subsingleton.elim _ hlocal.2 (E x) (E y))⟩

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.