NYLL
Module

UnitCohomologyAxiom.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.UnitCohomologyAxiom
30 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction: the unit-cohomology axiom

The coefficient group in the unit-cohomology axiom is the actual unit subgroup U_L, with the action of the actual quotient G_K / G_L. The two Tate groups are the homology objects of the finite-cyclic norm complexes.

Imports2
Imported by4

Declarations

structure

FiniteCyclicSubextension

L38 ↗
ClassFormation.FiniteCyclicSubextension
Documentation

A finite cyclic extension of a bundled finite abstract field. The generator and its cyclicity proof travel with the finite normal extension.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
section Generic
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · full declaration
structure FiniteCyclicSubextension (K : FiniteAbstractField G) where
  /-- The closed subgroup representing the top field. -/
  field : ClosedSubgroup G
  /-- The top-field subgroup is contained in the base-field subgroup. -/
  below : field.toSubgroup ≤ K.field.toSubgroup
  /-- The top-field subgroup is normal inside the base-field subgroup. -/
  normal : (extensionSubgroup K.field field below).Normal
  /-- The relative Galois quotient is finite. -/
  finite : Finite (K.field.toSubgroup ⧸
    extensionSubgroup K.field field below)
  /-- A chosen generator of the relative Galois quotient. -/
  generator : K.field.toSubgroup ⧸ extensionSubgroup K.field field below
  /-- Every quotient element is a power of the chosen generator. -/
  generates : ∀ x, x ∈ Subgroup.zpowers generator
def

toFiniteAbstractExtension

L60 ↗
ClassFormation.FiniteCyclicSubextension.toFiniteAbstractExtension
Documentation

Forget the cyclic generator and normality, retaining the underlying finite abstract extension.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
section Generic
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteCyclicSubextension
variable {K : FiniteAbstractField G}
Lean source · full declaration
def toFiniteAbstractExtension (E : FiniteCyclicSubextension K) :
    DegreeData.FiniteAbstractExtension G where
  field := E.field
  base := K.field
  below := E.below
  finiteQuotient := E.finite
def

IsUnramified

L68 ↗
ClassFormation.FiniteCyclicSubextension.IsUnramified
Documentation

Structural unramifiedness of the underlying finite extension.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
section Generic
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteCyclicSubextension
variable {K : FiniteAbstractField G}
Lean source · statement
def IsUnramified (E : FiniteCyclicSubextension K) (D : DegreeData G) : Prop
def

IsTotallyRamified

L72 ↗
ClassFormation.FiniteCyclicSubextension.IsTotallyRamified
Documentation

Structural total ramification of the underlying finite extension.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
section Generic
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteCyclicSubextension
variable {K : FiniteAbstractField G}
Lean source · statement
def IsTotallyRamified (E : FiniteCyclicSubextension K)
    (D : DegreeData G) : Prop
def

toFiniteAbstractFieldExtension

L79 ↗
ClassFormation.FiniteCyclicSubextension.toFiniteAbstractFieldExtension
Documentation

Retain the finite-over-base endpoint bundles as well as the relative finite quotient.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
section Generic
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteCyclicSubextension
variable {K : FiniteAbstractField G}
Lean source · statement
def toFiniteAbstractFieldExtension
    (E : FiniteCyclicSubextension K) : FiniteAbstractFieldExtension G
instance

(anonymous instance)

L87 ↗
Documentation

A finite cyclic subextension supplies normality of its representing subgroup.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
section Generic
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteCyclicSubextension
variable {K : FiniteAbstractField G}
Lean source · statement
instance (E : FiniteCyclicSubextension K) :
    (extensionSubgroup K.field E.field E.below).Normal
instance

(anonymous instance)

L92 ↗
Documentation

A finite cyclic subextension supplies finiteness of its Galois quotient.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
section Generic
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteCyclicSubextension
variable {K : FiniteAbstractField G}
Lean source · statement
instance (E : FiniteCyclicSubextension K) :
    Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field E.field E.below)
instance

(anonymous instance)

L97 ↗
Documentation

The finite quotient of a cyclic subextension carries its canonical Fintype.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
section Generic
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteCyclicSubextension
variable {K : FiniteAbstractField G}
Lean source · statement
instance (E : FiniteCyclicSubextension K) :
    Fintype (K.field.toSubgroup ⧸ extensionSubgroup K.field E.field E.below)
structure

FiniteUnramifiedCyclicExtension

L111 ↗
ClassFormation.FiniteUnramifiedCyclicExtension
Documentation

A finite cyclic extension together with the assertion that it is unramified for the fixed degree datum.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · full declaration
structure FiniteUnramifiedCyclicExtension
    (D : DegreeData G) (K : FiniteAbstractField G)
    extends FiniteCyclicSubextension K where
  /-- The underlying finite cyclic extension is unramified for `D`. -/
  unramified : toFiniteCyclicSubextension.IsUnramified D
def

toFiniteAbstractFieldExtension

L124 ↗
ClassFormation.FiniteUnramifiedCyclicExtension.toFiniteAbstractFieldExtension
Documentation

Forget cyclic and unramified structure while retaining both finite endpoint fields and the relative finite quotient.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace FiniteUnramifiedCyclicExtension
variable {K : FiniteAbstractField G}
Lean source · statement
def toFiniteAbstractFieldExtension
    (E : FiniteUnramifiedCyclicExtension D K) :
    FiniteAbstractFieldExtension G
theorem

toFiniteAbstractFieldExtension_isUnramified

L131 ↗
ClassFormation.FiniteUnramifiedCyclicExtension.toFiniteAbstractFieldExtension_isUnramified
Documentation

The unramified proof transported to the canonical finite field-extension bundle.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace FiniteUnramifiedCyclicExtension
variable {K : FiniteAbstractField G}
Lean source · statement
theorem toFiniteAbstractFieldExtension_isUnramified
    (E : FiniteUnramifiedCyclicExtension D K) :
    E.toFiniteAbstractFieldExtension.IsUnramified D
instance

(anonymous instance)

L137 ↗
Documentation

A finite unramified cyclic extension supplies normality of its representing subgroup.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace FiniteUnramifiedCyclicExtension
variable {K : FiniteAbstractField G}
Lean source · statement
instance (E : FiniteUnramifiedCyclicExtension D K) :
    (extensionSubgroup K.field E.field E.below).Normal
instance

(anonymous instance)

L142 ↗
Documentation

The quotient over K attached to a finite unramified cyclic extension is finite.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace FiniteUnramifiedCyclicExtension
variable {K : FiniteAbstractField G}
Lean source · statement
instance (E : FiniteUnramifiedCyclicExtension D K) :
    Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field E.field E.below)
instance

(anonymous instance)

L147 ↗
Documentation

The absolute quotient attached to a finite unramified cyclic extension is finite.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace FiniteUnramifiedCyclicExtension
variable {K : FiniteAbstractField G}
Lean source · statement
instance (E : FiniteUnramifiedCyclicExtension D K) :
    Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G) E.field (le_baseField E.field))
instance

(anonymous instance)

L154 ↗
Documentation

The finite quotient over K carries the canonical Fintype structure.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace FiniteUnramifiedCyclicExtension
variable {K : FiniteAbstractField G}
Lean source · statement
instance (E : FiniteUnramifiedCyclicExtension D K) :
    Fintype (K.field.toSubgroup ⧸ extensionSubgroup K.field E.field E.below)
def

fixedRepresentation

L166 ↗
ClassFormation.FiniteCyclicSubextension.fixedRepresentation
Documentation

The fixed coefficient representation attached to a bundled cyclic extension.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace FiniteCyclicSubextension
variable {K : FiniteAbstractField G}
Lean source · statement
def fixedRepresentation (E : FiniteCyclicSubextension K)
    (A : Rep ℤ G) :
    Rep ℤ (K.field.toSubgroup ⧸ extensionSubgroup K.field E.field E.below)
theorem

exists_norm_eq_of_tateHZero_isZero

L175 ↗
ClassFormation.exists_norm_eq_of_tateHZero_isZero
Documentation

Elementwise content of H⁰(Q,M)=0: every element fixed by a cyclic generator is an actual norm.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem exists_norm_eq_of_tateHZero_isZero
    {Q : IntegralRepGroupType} [Group Q] [Fintype Q]
    (M : Rep ℤ Q) (g : Q) (hg : ∀ x, x ∈ Subgroup.zpowers g)
    (hzero : Limits.IsZero (tateCohomology M 0)) :
    ∀ x : M.V, M.ρ g x = x → ∃ y : M.V, M.norm.hom y = x
theorem

valuationAt_normalExtensionAction

L199 ↗
ClassFormation.ValuationData.valuationAt_normalExtensionAction
Documentation

Normalized valuation is invariant under the Galois action in a finite tower. The proof uses transitivity of the actual norm and its invariance under the normal-extension action.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
theorem valuationAt_normalExtensionAction
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal)
    (k : E.base.field.toSubgroup)
    (a : ambientFixedAddSubgroup A E.field.field) :
    v.valuationAt E.field
        (normalExtensionAction A E.base.field E.field.field E.below
          hnormal k a) =
      v.valuationAt E.field a
def

unitActionLinearMap

L258 ↗
ClassFormation.ValuationData.unitActionLinearMap
Documentation

The action of G_K on the actual unit subgroup U_L.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · full declaration
def unitActionLinearMap
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal)
    (k : E.base.field.toSubgroup) :
    v.unitAddSubgroup E.field →ₗ[ℤ] v.unitAddSubgroup E.field where
  toFun u := ⟨normalExtensionAction A E.base.field E.field.field E.below
      hnormal k u.1, by
    rw [mem_unitAddSubgroup_iff,
      v.valuationAt_normalExtensionAction E hnormal k u.1]
    exact u.2⟩
  map_add' u w := by
    apply Subtype.ext
    apply Subtype.ext
    change A.ρ k.1 (u.1.1 + w.1.1) = A.ρ k.1 u.1.1 + A.ρ k.1 w.1.1
    exact map_add (A.ρ k.1) _ _
  map_smul' n u := by
    apply Subtype.ext
    apply Subtype.ext
    change A.ρ k.1 (n • u.1.1) = n • A.ρ k.1 u.1.1
    exact map_zsmul (A.ρ k.1) n u.1.1
def

unitRepresentationOverK

L280 ↗
ClassFormation.ValuationData.unitRepresentationOverK
Documentation

The G_K-representation on U_L before descending through G_L.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
def unitRepresentationOverK
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal) :
    Rep ℤ E.base.field.toSubgroup
theorem

unitRepresentationOverK_isTrivialOnExtension

L298 ↗
ClassFormation.ValuationData.unitRepresentationOverK_isTrivialOnExtension
Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
theorem unitRepresentationOverK_isTrivialOnExtension
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal) :
    Representation.IsTrivial
      ((v.unitRepresentationOverK E hnormal).ρ.comp
        (extensionSubgroup E.base.field E.field.field E.below).subtype)
def

unitRepresentation

L314 ↗
ClassFormation.ValuationData.unitRepresentation
Documentation

The actual quotient representation on the unit group U_L.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
def unitRepresentation
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal) :
    Rep ℤ (E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field E.field.field E.below)
def

unitRepresentation

L335 ↗
ClassFormation.FiniteUnramifiedCyclicExtension.unitRepresentation
Documentation

The unit representation carried by a bundled finite unramified cyclic extension.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace FiniteUnramifiedCyclicExtension
variable {K : FiniteAbstractField G}
Lean source · statement
def unitRepresentation
    (E : FiniteUnramifiedCyclicExtension D K) (v : ValuationData D A) :
    Rep ℤ (K.field.toSubgroup ⧸ extensionSubgroup K.field E.field E.below)
theorem

unitRepresentation_quotient_mk_apply

L346 ↗
ClassFormation.ValuationData.unitRepresentation_quotient_mk_apply
Documentation

The quotient unit representation acts on a representative through the original unit action.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
theorem unitRepresentation_quotient_mk_apply
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal)
    (k : E.base.field.toSubgroup) (u : v.unitAddSubgroup E.field) :
    (v.unitRepresentation E hnormal).ρ
        ((QuotientGroup.mk'
          (extensionSubgroup E.base.field E.field.field E.below)) k) u =
      v.unitActionLinearMap E hnormal k u
def

unitInclusion

L357 ↗
ClassFormation.ValuationData.unitInclusion
Documentation

Inclusion of units along an unramified finite extension.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · full declaration
def unitInclusion
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hUnramified : E.IsUnramified D) :
    v.unitAddSubgroup E.base →+ v.unitAddSubgroup E.field where
  toFun u := ⟨fixedFieldInclusion A E.base.field E.field.field E.below u.1, by
    rw [mem_unitAddSubgroup_iff]
    exact (v.valuationAt_fixedFieldInclusion_of_unramified E hUnramified u.1).trans
      u.2⟩
  map_zero' := by
    apply Subtype.ext
    rfl
  map_add' _ _ := by
    apply Subtype.ext
    rfl
theorem

unitRepresentation_action_coe

L374 ↗
ClassFormation.ValuationData.unitRepresentation_action_coe
Documentation

On underlying coefficients, the quotient action on U_L is the same coset action used in the relative norm.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
theorem unitRepresentation_action_coe
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal)
    (q : E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field E.field.field E.below)
    (u : v.unitAddSubgroup E.field) :
    (((v.unitRepresentation E hnormal).ρ q u).1 :
        ambientFixedAddSubgroup A E.field.field).1 =
      relativeCosetAction A E.base.field E.field.field E.below u.1 q
theorem

unitRepresentation_norm_coe

L390 ↗
ClassFormation.ValuationData.unitRepresentation_norm_coe
Documentation

The representation norm on U_L is the relative field norm on underlying coefficients.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · full declaration
theorem unitRepresentation_norm_coe
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal)
    (u : v.unitAddSubgroup E.field) :
    letI := Fintype.ofFinite
      (E.base.field.toSubgroup ⧸
        extensionSubgroup E.base.field E.field.field E.below)
    ((((v.unitRepresentation E hnormal).norm.hom u).1 :
        ambientFixedAddSubgroup A E.field.field) : A.V) =
      ((relativeNorm A E.base.field E.field.field E.below u.1 :
        ambientFixedAddSubgroup A E.base.field) : A.V) := by
  let := Fintype.ofFinite
    (E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field E.field.field E.below)
  rw [relativeNorm_apply_coe]
  change
    (((Representation.norm (v.unitRepresentation E hnormal).ρ) u).1 :
      ambientFixedAddSubgroup A E.field.field).1 =
      relativeNormValue A E.base.field E.field.field E.below u.1
  rw [Representation.norm, relativeNormValue]
  let coeToAmbient : v.unitAddSubgroup E.field →+ A.V :=
    (ambientFixedAddSubgroup A E.field.field).subtype.comp
      (v.unitAddSubgroup E.field).subtype
  change coeToAmbient
      ((∑ q, (v.unitRepresentation E hnormal).ρ q) u) =
    ∑ q, relativeCosetAction A E.base.field E.field.field E.below u.1 q
  refine (congrArg coeToAmbient (LinearMap.sum_apply Finset.univ
    (fun q : E.base.field.toSubgroup ⧸
        extensionSubgroup E.base.field E.field.field E.below =>
      (v.unitRepresentation E hnormal).ρ q) u)).trans ?_
  refine (map_sum coeToAmbient _ _).trans ?_
  apply Finset.sum_congr rfl
  intro q _
  exact v.unitRepresentation_action_coe E hnormal q u
theorem

exists_unit_relativeNorm_eq_of_tateHZero_isZero

L427 ↗
ClassFormation.ValuationData.exists_unit_relativeNorm_eq_of_tateHZero_isZero
Documentation

Actual H⁰=0 eliminator needed after the reciprocity construction: every unit of K is the relative norm of a unit of an unramified Galois extension L.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · full declaration
theorem exists_unit_relativeNorm_eq_of_tateHZero_isZero
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal)
    (hUnramified : E.IsUnramified D)
    (g : E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field E.field.field E.below)
    (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    letI := Fintype.ofFinite
      (E.base.field.toSubgroup ⧸
        extensionSubgroup E.base.field E.field.field E.below)
    Limits.IsZero
        (tateCohomology (v.unitRepresentation E hnormal) 0) →
      ∀ u : v.unitAddSubgroup E.base, ∃ ε : v.unitAddSubgroup E.field,
        relativeNorm A E.base.field E.field.field E.below ε.1 = u.1 := by
  let := Fintype.ofFinite
    (E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field E.field.field E.below)
  intro hzero u
  let U := v.unitRepresentation E hnormal
  let uL := v.unitInclusion E hUnramified u
  have hfixed : U.ρ g uL = uL := by
    refine Quotient.inductionOn' g ?_
    intro k
    apply Subtype.ext
    apply Subtype.ext
    change A.ρ k.1 u.1.1 = u.1.1
    exact u.1.2 k
  obtain ⟨ε, hε⟩ := exists_norm_eq_of_tateHZero_isZero
    U g hg hzero uL hfixed
  refine ⟨ε, ?_⟩
  apply Subtype.ext
  calc
    ((relativeNorm A E.base.field E.field.field E.below ε.1 :
        ambientFixedAddSubgroup A E.base.field) : A.V) =
        ((((v.unitRepresentation E hnormal).norm.hom ε).1 :
          ambientFixedAddSubgroup A E.field.field) : A.V) :=
      (v.unitRepresentation_norm_coe E hnormal ε).symm
    _ = ((uL.1 : ambientFixedAddSubgroup A E.field.field) : A.V) :=
      congrArg
        (fun z : v.unitAddSubgroup E.field =>
          ((z.1 : ambientFixedAddSubgroup A E.field.field) : A.V)) hε
    _ = u.1.1 := rfl
theorem

exists_unit_sigma_sub_eq_of_tateHMinusOne_isZero

L472 ↗
ClassFormation.ValuationData.exists_unit_sigma_sub_eq_of_tateHMinusOne_isZero
Documentation

Actual H⁻¹=0 eliminator on units: a unit of relative norm zero is in the image of g-1.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · full declaration
theorem exists_unit_sigma_sub_eq_of_tateHMinusOne_isZero
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup E.base.field E.field.field E.below).Normal)
    (g : E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field E.field.field E.below)
    (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    letI := Fintype.ofFinite
      (E.base.field.toSubgroup ⧸
        extensionSubgroup E.base.field E.field.field E.below)
    Limits.IsZero
        (tateCohomology (v.unitRepresentation E hnormal) (-1)) →
      ∀ u : (v.unitRepresentation E hnormal).V,
        (v.unitRepresentation E hnormal).norm.hom u = 0 →
        ∃ ε : (v.unitRepresentation E hnormal).V,
          (v.unitRepresentation E hnormal).ρ g ε - ε = u := by
  let := Fintype.ofFinite
    (E.base.field.toSubgroup ⧸
      extensionSubgroup E.base.field E.field.field E.below)
  intro hzero u hu
  let U := v.unitRepresentation E hnormal
  exact CyclicCohomology.normKernel_le_sigmaMinusOneRange_of_tateHMinusOne_isZero
    U g hg hzero u hu
def

SatisfiesUnramifiedUnitCohomology

L501 ↗
ClassFormation.ValuationData.SatisfiesUnramifiedUnitCohomology
Documentation

the unit-cohomology axiom. For every finite unramified Galois extension L/K, H⁰(G(L/K),U_L) and H⁻¹(G(L/K),U_L) vanish.

This is a predicate on the abstract valuation datum. It is the source axiom used in the subsequent proofs of independence and multiplicativity in ; it is not introduced as a Lean axiom.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
universe u
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
def SatisfiesUnramifiedUnitCohomology
    (D : DegreeData G) (v : ValuationData D A) : Prop

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