NYLL
Module

MainNaturality.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.MainNaturality
41 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction, norm--conjugation naturality: naturality of reciprocity

The two vertical maps are constructed here on the actual finite Galois quotients and the actual finite norm quotients. Their defining commutativities are proved from norm transitivity and conjugation, so the eventual the finite reciprocity equivalence reciprocity homomorphisms can be connected without any additional comparison datum.

Mathlib's Rep ℤ G forces its representation-bearing group G to Type 0.

Mathlib's Rep ℤ G forces its representation-bearing group G to Type 0.

Imports1
Imported by2

Declarations

def

finiteReciprocityNaturalityRestriction

L42 ↗
ClassFormation.finiteReciprocityNaturalityRestriction
Documentation

The left vertical map in the first diagram of norm--conjugation naturality: restriction from G(L'/K') to G(L/K).

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def finiteReciprocityNaturalityRestriction
    (K K' L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    [hL'normal : (extensionSubgroup K' L' hL'K').Normal] :
    (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K') →*
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)
theorem

finiteReciprocityNaturalityRestriction_mk

L64 ↗
ClassFormation.finiteReciprocityNaturalityRestriction_mk
Documentation

Restriction sends a represented finite reciprocity class to the corresponding lower-level class.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem finiteReciprocityNaturalityRestriction_mk
    (K K' L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    [hL'normal : (extensionSubgroup K' L' hL'K').Normal]
    (k' : K'.toSubgroup) :
    finiteReciprocityNaturalityRestriction K K' L L' hLK hL'K' hK'K hL'L
        (QuotientGroup.mk k') =
      QuotientGroup.mk (Subgroup.inclusion hK'K k')
def

finiteReciprocityNaturalityFrobeniusTowerMap

L82 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusTowerMap
Documentation

Restriction on the infinite Frobenius quotients underlying the first diagram of norm--conjugation naturality.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def finiteReciprocityNaturalityFrobeniusTowerMap
    (D : DegreeData G) [IsTopologicalGroup G]
    (K K' L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    [hL'normal : (extensionSubgroup K' L' hL'K').Normal] :
    (K'.toSubgroup ⧸ D.extensionInertiaWithin K' L' hL'K') →*
      (K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK)
theorem

finiteReciprocityNaturalityFrobeniusTowerMap_mk

L106 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusTowerMap_mk
Documentation

The Frobenius tower map has the expected value on a quotient representative.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusTowerMap_mk
    (D : DegreeData G) [IsTopologicalGroup G]
    (K K' L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    [hL'normal : (extensionSubgroup K' L' hL'K').Normal]
    (k' : K'.toSubgroup) :
    D.finiteReciprocityNaturalityFrobeniusTowerMap K K' L L'
        hLK hL'K' hK'K hL'L (QuotientGroup.mk k') =
      QuotientGroup.mk (Subgroup.inclusion hK'K k')
def

finiteReciprocityNaturalityFrobeniusTowerMapContinuous

L122 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusTowerMapContinuous
Documentation

Continuous form of finiteReciprocityNaturalityFrobeniusTowerMap, used to transport the closed cyclic subgroup generated by a Frobenius lift.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · full declaration
def finiteReciprocityNaturalityFrobeniusTowerMapContinuous
    (D : DegreeData G) [IsTopologicalGroup G]
    (K K' L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal]
    [hL'normal : (extensionSubgroup K' L' hL'K').Normal] :
    (K'.toSubgroup ⧸ D.extensionInertiaWithin K' L' hL'K') →ₜ*
      (K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK) where
  toMonoidHom := D.finiteReciprocityNaturalityFrobeniusTowerMap
    K K' L L' hLK hL'K' hK'K hL'L
  continuous_toFun := by
    rw [← QuotientGroup.isOpenQuotientMap_mk.continuous_comp_iff]
    change Continuous (fun k' : K'.toSubgroup =>
      QuotientGroup.mk (Subgroup.inclusion hK'K k'))
    apply QuotientGroup.continuous_mk.comp
    exact continuous_subtype_val.subtype_mk _
theorem

finiteReciprocityNaturalityFrobeniusTowerMap_degree

L144 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusTowerMap_degree
Documentation

Frobenius residue-degree compatibility's normalized-degree square on the two infinite Frobenius quotients.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusTowerMap_degree
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.FiniteResidueAbstractExtension D)
    (L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ E.base.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ E.field.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup E.base.field L hLK).Normal]
    [hL'normal : (extensionSubgroup E.field.field L' hL'K').Normal]
    (q : E.field.toSubgroup ⧸
      D.extensionInertiaWithin E.field.field L' hL'K') :
    (D.extensionNormalizedDegree E.base L hLK
      (D.finiteReciprocityNaturalityFrobeniusTowerMap
        E.base.field E.field.field L L'
        hLK hL'K' E.below hL'L q)).toAdd =
      (E.residueDegree : ℕ) •
        (D.extensionNormalizedDegree E.field L' hL'K' q).toAdd
def

finiteReciprocityNaturalityFrobeniusTowerLift

L169 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusTowerLift
Documentation

A positive Frobenius lift over K' remains a positive Frobenius lift over K; its exponent is multiplied by f_{K'/K}.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def finiteReciprocityNaturalityFrobeniusTowerLift
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.FiniteResidueAbstractExtension D)
    (L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ E.base.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ E.field.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup E.base.field L hLK).Normal]
    [hL'normal : (extensionSubgroup E.field.field L' hL'K').Normal]
    (σ : D.FrobeniusElements E.field L' hL'K') :
    D.FrobeniusElements E.base L hLK
theorem

finiteReciprocityNaturalityFrobeniusTowerLift_coe

L195 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusTowerLift_coe
Documentation

The chosen Frobenius tower lift coerces to the represented ambient automorphism.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusTowerLift_coe
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.FiniteResidueAbstractExtension D)
    (L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ E.base.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ E.field.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup E.base.field L hLK).Normal]
    [hL'normal : (extensionSubgroup E.field.field L' hL'K').Normal]
    (σ : D.FrobeniusElements E.field L' hL'K') :
    (D.finiteReciprocityNaturalityFrobeniusTowerLift
      E L L' hLK hL'K' hL'L σ).1 =
      D.finiteReciprocityNaturalityFrobeniusTowerMap
        E.base.field E.field.field L L' hLK hL'K' E.below hL'L σ.1
theorem

finiteReciprocityNaturalityFrobeniusTowerLift_exponent

L213 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusTowerLift_exponent
Documentation

The Frobenius tower lift has the prescribed Frobenius exponent.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusTowerLift_exponent
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.FiniteResidueAbstractExtension D)
    (L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ E.base.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ E.field.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup E.base.field L hLK).Normal]
    [hL'normal : (extensionSubgroup E.field.field L' hL'K').Normal]
    (σ : D.FrobeniusElements E.field L' hL'K') :
    D.frobeniusExponent E.base L hLK
        (D.finiteReciprocityNaturalityFrobeniusTowerLift
          E L L' hLK hL'K' hL'L σ) =
      (E.residueDegree : ℕ) *
        D.frobeniusExponent E.field L' hL'K' σ
theorem

finiteReciprocityNaturalityRestriction_frobeniusTowerLift

L255 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityRestriction_frobeniusTowerLift
Documentation

Restriction of the transported lift is the restriction of the original lift along the left vertical map of norm--conjugation naturality.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityRestriction_frobeniusTowerLift
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.FiniteResidueAbstractExtension D)
    (L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ E.base.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ E.field.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup E.base.field L hLK).Normal]
    [hL'normal : (extensionSubgroup E.field.field L' hL'K').Normal]
    (σ : D.FrobeniusElements E.field L' hL'K') :
    finiteReciprocityNaturalityRestriction
        E.base.field E.field.field L L' hLK hL'K' E.below hL'L
        (D.frobeniusRestriction E.field L' hL'K' σ) =
      D.frobeniusRestriction E.base L hLK
        (D.finiteReciprocityNaturalityFrobeniusTowerLift
          E L L' hLK hL'K' hL'L σ)
theorem

finiteReciprocityNaturalityFrobeniusFixedField_le

L284 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusFixedField_le
Documentation

The fixed field of a transported Frobenius lift contains the original fixed field, i.e. Σ' / Σ is an intermediate extension.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusFixedField_le
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : DegreeData.FiniteResidueAbstractExtension D)
    (L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ E.base.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ E.field.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup E.base.field L hLK).Normal]
    [hL'normal : (extensionSubgroup E.field.field L' hL'K').Normal]
    (σ : D.FrobeniusElements E.field L' hL'K') :
    (D.frobeniusFixedField E.field L' hL'K' σ).toSubgroup ≤
      (D.frobeniusFixedField E.base L hLK
        (D.finiteReciprocityNaturalityFrobeniusTowerLift
          E L L' hLK hL'K' hL'L σ)).toSubgroup
theorem

finiteReciprocityNaturalityFrobeniusFixedField_isTotallyRamified

L323 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusFixedField_isTotallyRamified
Documentation

The intermediate extension Σ' / Σ attached to a transported Frobenius lift is totally ramified.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusFixedField_isTotallyRamified
    (D : DegreeData G) [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (E : DegreeData.FiniteResidueAbstractExtension D)
    (L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ E.base.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ E.field.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup E.base.field L hLK).Normal]
    [hL'normal : (extensionSubgroup E.field.field L' hL'K').Normal]
    [Finite
      (E.base.toSubgroup ⧸ extensionSubgroup E.base.field L hLK)]
    [hL'K'finite : Finite
      (E.field.toSubgroup ⧸ extensionSubgroup E.field.field L' hL'K')]
    (σ : D.FrobeniusElements E.field L' hL'K') :
    (DegreeData.AbstractExtension.mk
      (D.frobeniusFixedField E.field L' hL'K' σ)
      (D.frobeniusFixedField E.base L hLK
        (D.finiteReciprocityNaturalityFrobeniusTowerLift
          E L L' hLK hL'K' hL'L σ))
      (D.finiteReciprocityNaturalityFrobeniusFixedField_le
        E L L' hLK hL'K' hL'L σ)).IsTotallyRamified D
theorem

finiteReciprocityNaturality_tower_finite

L405 ↗
ClassFormation.finiteReciprocityNaturality_tower_finite
Documentation

Finiteness of the upper-left-to-lower-right composite extension in the first diagram.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem finiteReciprocityNaturality_tower_finite
    (K K' L' : ClosedSubgroup G)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K K' hK'K)]
    [Finite (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')] :
    Finite (K.toSubgroup ⧸
      extensionSubgroup K L' (hL'K'.trans hK'K))
def

finiteReciprocityNaturalityNormMap

L424 ↗
ClassFormation.finiteReciprocityNaturalityNormMap
Documentation

The right vertical map in the first diagram of norm--conjugation naturality. It is the actual norm N_{K'/K}, descended to the actual finite norm quotients.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def finiteReciprocityNaturalityNormMap
    (A : Rep ℤ G) (K K' L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLKfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hL'K'finite : Finite
      (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')]
    [hK'Kfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K K' hK'K)] :
    FiniteNormQuotient A K' L' hL'K' →+
      FiniteNormQuotient A K L hLK
theorem

finiteReciprocityNaturalityNormMap_finiteNormClass

L478 ↗
ClassFormation.finiteReciprocityNaturalityNormMap_finiteNormClass
Documentation

The norm map carries a finite norm class to the corresponding class over the base.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem finiteReciprocityNaturalityNormMap_finiteNormClass
    (A : Rep ℤ G) (K K' L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLKfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [Finite
      (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')]
    [hK'Kfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K K' hK'K)]
    (a : ambientFixedAddSubgroup A K') :
    finiteReciprocityNaturalityNormMap A K K' L L' hLK hL'K' hK'K hL'L
        (finiteNormClass A K' L' hL'K' a) =
      finiteNormClass A K L hLK (relativeNorm A K K' hK'K a)
def

conjugateFixedElementHom

L499 ↗
ClassFormation.conjugateFixedElementHom
Documentation

The additive map a ↦ a^s between the two actual fixed subgroups.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
def conjugateFixedElementHom [ContinuousMul G]
    (A : Rep ℤ G) (K : ClosedSubgroup G) (s : G) :
    ambientFixedAddSubgroup A K →+
      ambientFixedAddSubgroup A (conjugateClosedSubgroup K s) where
  toFun := conjugateFixedElement A K s
  map_zero' := by
    apply Subtype.ext
    exact map_zero (A.ρ s⁻¹)
  map_add' a b := by
    apply Subtype.ext
    exact map_add (A.ρ s⁻¹) a.1 b.1
theorem

conjugateFixedElementHom_apply

L513 ↗
ClassFormation.conjugateFixedElementHom_apply
Documentation

The homomorphism on conjugate-fixed elements evaluates by the underlying conjugation map.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem conjugateFixedElementHom_apply [ContinuousMul G]
    (A : Rep ℤ G) (K : ClosedSubgroup G) (s : G)
    (a : ambientFixedAddSubgroup A K) :
    conjugateFixedElementHom A K s a = conjugateFixedElement A K s a
def

finiteReciprocityNaturalityConjugationNormMap

L521 ↗
ClassFormation.finiteReciprocityNaturalityConjugationNormMap
Documentation

The right vertical map in the conjugation diagram of norm--conjugation naturality, descended to the actual finite norm quotients.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
def finiteReciprocityNaturalityConjugationNormMap
    [ContinuousMul G] (A : Rep ℤ G)
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    [hLfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)] :
    letI : Finite ((conjugateClosedSubgroup K s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s)) :=
      finite_conjugateExtension K L hLK s
    FiniteNormQuotient A K L hLK →+
      FiniteNormQuotient A (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s) := by
  letI hConjFinite : Finite ((conjugateClosedSubgroup K s).toSubgroup ⧸
      extensionSubgroup (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)) :=
    finite_conjugateExtension K L hLK s
  let f : ambientFixedAddSubgroup A K →+
      FiniteNormQuotient A (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s) :=
    (finiteNormClassHom A (conjugateClosedSubgroup K s)
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s)).comp
        (conjugateFixedElementHom A K s)
  apply finiteNormQuotientLift A K L hLK f
  rintro _ ⟨a, rfl⟩
  apply (finiteNormClass_eq_zero_iff A (conjugateClosedSubgroup K s)
    (conjugateClosedSubgroup L s) (conjugateClosedSubgroup_mono hLK s) _).2
  refine ⟨conjugateFixedElement A L s a, ?_⟩
  exact relativeNorm_conjugate_apply A K L hLK s a
theorem

finiteReciprocityNaturalityConjugationNormMap_finiteNormClass

L558 ↗
ClassFormation.finiteReciprocityNaturalityConjugationNormMap_finiteNormClass
Documentation

The conjugation norm map preserves canonical finite norm classes.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
theorem finiteReciprocityNaturalityConjugationNormMap_finiteNormClass
    [ContinuousMul G] (A : Rep ℤ G)
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (a : ambientFixedAddSubgroup A K) :
    letI : Finite ((conjugateClosedSubgroup K s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s)) :=
      finite_conjugateExtension K L hLK s
    finiteReciprocityNaturalityConjugationNormMap A K L hLK s
        (finiteNormClass A K L hLK a) =
      finiteNormClass A (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s) (conjugateClosedSubgroup_mono hLK s)
        (conjugateFixedElement A K s a) := by
  let hConjFinite : Finite ((conjugateClosedSubgroup K s).toSubgroup ⧸
      extensionSubgroup (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)) :=
    finite_conjugateExtension K L hLK s
  simp [finiteReciprocityNaturalityConjugationNormMap]
  rfl
theorem

finiteReciprocityNaturality_norm_tower_class

L585 ↗
ClassFormation.finiteReciprocityNaturality_norm_tower_class
Documentation

The norm identity used for the first diagram of norm--conjugation naturality, already expressed in the target finite norm quotient. Taking S = Σ and S' = Σ' gives the calculation.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem finiteReciprocityNaturality_norm_tower_class
    (A : Rep ℤ G)
    (K K' L L' S S' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hS'K' : S'.toSubgroup ≤ K'.toSubgroup)
    (hS'S : S'.toSubgroup ≤ S.toSubgroup)
    [hLKfinite : Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [hL'K'finite : Finite (K'.toSubgroup ⧸ extensionSubgroup K' L' hL'K')]
    [hK'Kfinite : Finite (K.toSubgroup ⧸ extensionSubgroup K K' hK'K)]
    [hSKfinite : Finite (K.toSubgroup ⧸ extensionSubgroup K S hSK)]
    [hS'K'finite : Finite (K'.toSubgroup ⧸ extensionSubgroup K' S' hS'K')]
    [hS'Sfinite : Finite (S.toSubgroup ⧸ extensionSubgroup S S' hS'S)]
    (π : ambientFixedAddSubgroup A S') :
    finiteReciprocityNaturalityNormMap A K K' L L' hLK hL'K' hK'K hL'L
        (finiteNormClass A K' L' hL'K'
          (relativeNorm A K' S' hS'K' π)) =
      finiteNormClass A K L hLK
        (relativeNorm A K S hSK (relativeNorm A S S' hS'S π))
theorem

finiteReciprocityNaturality_restriction_norm_commutes

L642 ↗
ClassFormation.DegreeData.finiteReciprocityNaturality_restriction_norm_commutes
Documentation

norm--conjugation naturality, first diagram. Restriction on finite Galois groups corresponds under the finite reciprocity equivalence to the norm N_{K'/K} on finite norm quotients.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturality_restriction_norm_commutes
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (E : FiniteAbstractFieldExtension G)
    (L L' : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ E.base.field.toSubgroup)
    (hL'K' : L'.toSubgroup ≤ E.field.field.toSubgroup)
    (hL'L : L'.toSubgroup ≤ L.toSubgroup)
    [hLnormal : (extensionSubgroup E.base.field L hLK).Normal]
    [hL'normal : (extensionSubgroup E.field.field L' hL'K').Normal]
    [hLKfinite : Finite
      (E.base.field.toSubgroup ⧸ extensionSubgroup E.base.field L hLK)]
    [hL'K'finite : Finite
      (E.field.field.toSubgroup ⧸
        extensionSubgroup E.field.field L' hL'K')] :
    (finiteReciprocityNaturalityNormMap A E.base.field E.field.field L L'
      hLK hL'K' E.below hL'L).comp
        (D.finiteReciprocityHom A v hAxiom E.field L' hL'K') =
      (D.finiteReciprocityHom A v hAxiom E.base L hLK).comp
      (finiteReciprocityNaturalityRestriction
          E.base.field E.field.field L L'
          hLK hL'K' E.below hL'L).toAdditive
theorem

finiteReciprocityNaturality_conjugation_norm_class

L797 ↗
ClassFormation.finiteReciprocityNaturality_conjugation_norm_class
Documentation

The norm identity used for the second diagram of norm--conjugation naturality, expressed in the conjugate finite norm quotient.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
theorem finiteReciprocityNaturality_conjugation_norm_class
    [ContinuousMul G] (A : Rep ℤ G)
    (K L S : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hSK : S.toSubgroup ≤ K.toSubgroup) (s : G)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    [Finite (K.toSubgroup ⧸ extensionSubgroup K S hSK)]
    (π : ambientFixedAddSubgroup A S) :
    let hConjLK := conjugateClosedSubgroup_mono hLK s
    let hConjSK := conjugateClosedSubgroup_mono hSK s
    letI : Finite ((conjugateClosedSubgroup K s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s) hConjLK) :=
      finite_conjugateExtension K L hLK s
    letI : Finite ((conjugateClosedSubgroup K s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup S s) hConjSK) :=
      finite_conjugateExtension K S hSK s
    finiteReciprocityNaturalityConjugationNormMap A K L hLK s
        (finiteNormClass A K L hLK
          (relativeNorm A K S hSK π)) =
      finiteNormClass A (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s) hConjLK
        (relativeNorm A (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup S s) hConjSK
          (conjugateFixedElement A S s π)) := by
  dsimp only
  rw [finiteReciprocityNaturalityConjugationNormMap_finiteNormClass,
    relativeNorm_conjugate_apply]
theorem

finiteReciprocityNaturalityDegree_conjugateSubgroupEquiv

L836 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityDegree_conjugateSubgroupEquiv
Documentation

The global degree is invariant under conjugation.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityDegree_conjugateSubgroupEquiv
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : ClosedSubgroup G) (s : G) (k : K.toSubgroup) :
    D.degree (conjugateSubgroupEquiv K s k).1 = D.degree k.1
theorem

finiteReciprocityNaturalityNormalizedDegree_conjugateSubgroupEquiv

L845 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityNormalizedDegree_conjugateSubgroupEquiv
Documentation

The normalized degree is invariant under the conjugation equivalence of field subgroups.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityNormalizedDegree_conjugateSubgroupEquiv
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (s : G)
    (k : K.field.toSubgroup) :
    D.normalizedDegree (K.conjugate s : D.FiniteResidueAbstractField)
        (conjugateSubgroupEquiv K.field s k) =
      D.normalizedDegree K k
theorem

finiteReciprocityNaturalityMap_extensionInertiaWithin_conjugate

L869 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityMap_extensionInertiaWithin_conjugate
Documentation

Conjugation carries I_L inside G_K exactly to the corresponding inertia subgroup for L^s / K^s.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityMap_extensionInertiaWithin_conjugate
    (D : DegreeData G) [IsTopologicalGroup G]
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G) :
    (D.extensionInertiaWithin K L hLK).map
        (conjugateSubgroupEquiv K s).toMonoidHom =
      D.extensionInertiaWithin (conjugateClosedSubgroup K s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
def

finiteReciprocityNaturalityFrobeniusConjugationEquiv

L912 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusConjugationEquiv
Documentation

Conjugation as a continuous multiplicative equivalence on the infinite Frobenius quotients.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def finiteReciprocityNaturalityFrobeniusConjugationEquiv
    (D : DegreeData G) [IsTopologicalGroup G]
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K L hLK).Normal] :
    (K.toSubgroup ⧸ D.extensionInertiaWithin K L hLK) ≃ₜ*
      ((conjugateClosedSubgroup K s).toSubgroup ⧸
        D.extensionInertiaWithin (conjugateClosedSubgroup K s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s))
theorem

finiteReciprocityNaturalityFrobeniusConjugationEquiv_mk

L961 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusConjugationEquiv_mk
Documentation

The Frobenius conjugation equivalence has the expected value on quotient representatives.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusConjugationEquiv_mk
    (D : DegreeData G) [IsTopologicalGroup G]
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) (s : G)
    [(extensionSubgroup K L hLK).Normal]
    (k : K.toSubgroup) :
    D.finiteReciprocityNaturalityFrobeniusConjugationEquiv K L hLK s
        (QuotientGroup.mk k) =
      QuotientGroup.mk (conjugateSubgroupEquiv K s k)
instance

finiteReciprocityNaturalityFiniteResidueConjugate_normal

L981 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFiniteResidueConjugate_normal
Documentation

The normality transported by conjugation is exposed at the residue-finite field boundary. Keeping this bridge as an instance prevents clients from unfolding the bundled conjugate merely to recover the existing normality instance for the literal conjugate subgroup.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
instance finiteReciprocityNaturalityFiniteResidueConjugate_normal
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    (extensionSubgroup (K.conjugate s).field
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s)).Normal
theorem

finiteReciprocityNaturalityFrobeniusConjugationEquiv_degree

L996 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusConjugationEquiv_degree
Documentation

The conjugation equivalence preserves normalized degree.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusConjugationEquiv_degree
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK) :
    D.extensionNormalizedDegree
        (K.conjugate s : D.FiniteResidueAbstractField)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (D.finiteReciprocityNaturalityFrobeniusConjugationEquiv K.field L hLK s q) =
      D.extensionNormalizedDegree K L hLK q
def

finiteReciprocityNaturalityFrobeniusConjugationLift

L1018 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusConjugationLift
Documentation

Conjugation transports positive Frobenius lifts without changing their exponent.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def finiteReciprocityNaturalityFrobeniusConjugationLift
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK) :
    D.FrobeniusElements (K.conjugate s : D.FiniteResidueAbstractField)
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s)
theorem

finiteReciprocityNaturalityFrobeniusConjugationLift_coe

L1035 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusConjugationLift_coe
Documentation

The Frobenius conjugation lift has the stated ambient coercion.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusConjugationLift_coe
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK) :
    (D.finiteReciprocityNaturalityFrobeniusConjugationLift K L hLK s σ).1 =
      D.finiteReciprocityNaturalityFrobeniusConjugationEquiv K.field L hLK s σ.1
theorem

finiteReciprocityNaturalityFrobeniusConjugationLift_exponent

L1047 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusConjugationLift_exponent
Documentation

The Frobenius conjugation lift preserves the selected exponent.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusConjugationLift_exponent
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK) :
    D.frobeniusExponent (K.conjugate s : D.FiniteResidueAbstractField)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (D.finiteReciprocityNaturalityFrobeniusConjugationLift K L hLK s σ) =
      D.frobeniusExponent K L hLK σ
theorem

finiteReciprocityNaturalityConjugateInertia_normal

L1085 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityConjugateInertia_normal
Source context 11 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
section ConjugateFrobeniusQuotients
Lean source · statement
theorem finiteReciprocityNaturalityConjugateInertia_normal
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    (D.extensionInertiaWithin (K.conjugate s).field
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s)).Normal
theorem

finiteReciprocityNaturalityFrobeniusConjugationEquiv_mem_closure_iff

L1104 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusConjugationEquiv_mem_closure_iff
Documentation

The continuous conjugation equivalence identifies the two closed cyclic subgroups generated by corresponding Frobenius lifts.

Source context 12 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
section ConjugateFrobeniusQuotients
attribute [local instance] finiteReciprocityNaturalityConjugateInertia_normal
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusConjugationEquiv_mem_closure_iff
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK)
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK) :
    q ∈ (D.frobeniusClosure K L hLK σ).toSubgroup ↔
      D.finiteReciprocityNaturalityFrobeniusConjugationEquiv K.field L hLK s q ∈
        (D.frobeniusClosure
          (K.conjugate s : D.FiniteResidueAbstractField)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s)
          (D.finiteReciprocityNaturalityFrobeniusConjugationLift
            K L hLK s σ)).toSubgroup
theorem

finiteReciprocityNaturalityConjugation_frobeniusRestriction

L1147 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityConjugation_frobeniusRestriction
Documentation

Conjugation of a Frobenius lift commutes with restriction to the finite Galois quotient.

Source context 12 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
section ConjugateFrobeniusQuotients
attribute [local instance] finiteReciprocityNaturalityConjugateInertia_normal
Lean source · statement
theorem finiteReciprocityNaturalityConjugation_frobeniusRestriction
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK) :
    finiteReciprocityNaturalityConjugation K.field L hLK s
        (D.frobeniusRestriction K L hLK σ) =
      D.frobeniusRestriction
        (K.conjugate s : D.FiniteResidueAbstractField)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (D.finiteReciprocityNaturalityFrobeniusConjugationLift K L hLK s σ)
theorem

finiteReciprocityNaturalityFrobeniusFixedField_conjugate

L1174 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFrobeniusFixedField_conjugate
Documentation

The fixed field of the conjugated Frobenius lift is the conjugate of the original fixed field.

Source context 12 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
section ConjugateFrobeniusQuotients
attribute [local instance] finiteReciprocityNaturalityConjugateInertia_normal
Lean source · statement
theorem finiteReciprocityNaturalityFrobeniusFixedField_conjugate
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK) :
    conjugateClosedSubgroup (D.frobeniusFixedField K L hLK σ) s =
      D.frobeniusFixedField
        (K.conjugate s : D.FiniteResidueAbstractField)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (D.finiteReciprocityNaturalityFrobeniusConjugationLift K L hLK s σ)
instance

finiteReciprocityNaturalityFiniteAbstractConjugate_normal

L1285 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityFiniteAbstractConjugate_normal
Documentation

Normality of a conjugated finite abstract field is available without unfolding the finite-field bundle.

Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
instance finiteReciprocityNaturalityFiniteAbstractConjugate_normal
    [IsTopologicalGroup G]
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal] :
    (extensionSubgroup (K.conjugate s).field
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s)).Normal
theorem

finiteReciprocityNaturality_isPrimeElement_transport

L1299 ↗
ClassFormation.DegreeData.finiteReciprocityNaturality_isPrimeElement_transport
Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturality_isPrimeElement_transport
    (D : DegreeData G) {A : Rep ℤ G} (v : ValuationData D A)
    (S T : FiniteAbstractField G) (hST : S.field = T.field)
    (π : ambientFixedAddSubgroup A S.field) (hπ : v.IsPrimeElement S π) :
    v.IsPrimeElement T (hST ▸ π)
theorem

finiteReciprocityNaturality_relativeNorm_right_transport

L1309 ↗
ClassFormation.DegreeData.finiteReciprocityNaturality_relativeNorm_right_transport
Source context 10 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteReciprocityNaturality_relativeNorm_right_transport
    (A : Rep ℤ G) (K S T : ClosedSubgroup G) (hST : S = T)
    (hSK : S.toSubgroup ≤ K.toSubgroup)
    (hTK : T.toSubgroup ≤ K.toSubgroup)
    [hKSfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K S hSK)]
    [hKTfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K T hTK)]
    (π : ambientFixedAddSubgroup A S) :
    relativeNorm A K S hSK π =
      relativeNorm A K T hTK (hST ▸ π)
def

finiteReciprocityNaturalityConjugateNormAddZero

L1326 ↗
ClassFormation.DegreeData.finiteReciprocityNaturalityConjugateNormAddZero
Source context 11 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
section ConjugateFiniteNormQuotient
Lean source · statement
def finiteReciprocityNaturalityConjugateNormAddZero
    (A : Rep ℤ G) [IsTopologicalGroup G]
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
theorem

finiteReciprocityNaturality_conjugation_commutes

L1349 ↗
ClassFormation.DegreeData.finiteReciprocityNaturality_conjugation_commutes
Documentation

norm--conjugation naturality, second diagram. Conjugation of finite Galois groups corresponds under the finite reciprocity equivalence to conjugation of finite norm classes.

Source context 12 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
section Representation
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
section ConjugateFiniteNormQuotient
attribute [local instance] finiteReciprocityNaturalityConjugateNormAddZero
Lean source · full declaration
theorem finiteReciprocityNaturality_conjugation_commutes
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup) (s : G)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)] :
    let Ks : FiniteAbstractField G := K.conjugate s
    let Ls := conjugateClosedSubgroup L s
    let hLsKs := conjugateClosedSubgroup_mono hLK s
    letI : Finite
        (Ks.field.toSubgroup ⧸ extensionSubgroup Ks.field Ls hLsKs) :=
      finite_conjugateExtension K.field L hLK s
    (finiteReciprocityNaturalityConjugationNormMap A K.field L hLK s).comp
        (D.finiteReciprocityHom A v hAxiom K L hLK) =
      (D.finiteReciprocityHom A v hAxiom Ks Ls hLsKs).comp
        (finiteReciprocityNaturalityConjugation K.field L hLK s).toMonoidHom.toAdditive := by
  dsimp only
  let hLsfinite : Finite
      ((conjugateClosedSubgroup K.field s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K.field s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s)) :=
    finite_conjugateExtension K.field L hLK s
  let KR : D.FiniteResidueAbstractField :=
    K.toFiniteResidueAbstractField D
  let Ks : FiniteAbstractField G := K.conjugate s
  let KRs : D.FiniteResidueAbstractField :=
    Ks.toFiniteResidueAbstractField D
  have hKRs_conjugate : KR.conjugate s = KRs := by
    dsimp [KRs, Ks, KR]
    unfold FiniteAbstractField.toFiniteResidueAbstractField
    unfold FiniteAbstractField.conjugate
    unfold DegreeData.FiniteResidueAbstractField.conjugate
    rfl
  let hLsfiniteKs : Finite
      (Ks.field.toSubgroup ⧸
        extensionSubgroup Ks.field (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s)) := by
    change Finite
      ((conjugateClosedSubgroup K.field s).toSubgroup ⧸
        extensionSubgroup (conjugateClosedSubgroup K.field s)
          (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s))
    exact hLsfinite
  let hLsfiniteKRs : Finite
      (KRs.field.toSubgroup ⧸
        extensionSubgroup KRs.field (conjugateClosedSubgroup L s)
          (conjugateClosedSubgroup_mono hLK s)) := by
    simpa only [KRs, FiniteAbstractField.toFiniteResidueAbstractField] using
      hLsfiniteKs
  let hLnormalKR : (extensionSubgroup KR.field L hLK).Normal := by
    simpa only [KR, FiniteAbstractField.toFiniteResidueAbstractField] using
      hLnormal
  let hLsnormalKs :
      (extensionSubgroup Ks.field (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)).Normal := by
    change
      (extensionSubgroup (conjugateClosedSubgroup K.field s)
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)).Normal
    infer_instance
  let hLsnormalKRs :
      (extensionSubgroup KRs.field (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)).Normal := by
    simpa only [KRs, FiniteAbstractField.toFiniteResidueAbstractField] using
      hLsnormalKs
  apply AddMonoidHom.ext
  intro q
  let σ := D.chosenFiniteReciprocityFrobeniusLift KR L hLK q.toMul
  let σs : D.FrobeniusElements KRs
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s) := by
    subst KRs
    exact D.finiteReciprocityNaturalityFrobeniusConjugationLift
      KR L hLK s σ
  have hσ : D.frobeniusRestriction KR L hLK σ = q.toMul :=
    D.frobeniusRestriction_chosenFiniteReciprocityFrobeniusLift
      KR L hLK q.toMul
  have hσs : D.frobeniusRestriction KRs
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s) σs =
      ((finiteReciprocityNaturalityConjugation
        K.field L hLK s).toMonoidHom.toAdditive q).toMul := by
    change D.frobeniusRestriction KRs
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s) σs =
      finiteReciprocityNaturalityConjugation K.field L hLK s q.toMul
    rw [← hσ]
    symm
    change finiteReciprocityNaturalityConjugation K.field L hLK s
        (D.extensionRestriction KR.field L hLK σ.1) =
      D.extensionRestriction KRs.field
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s) σs.1
    unfold σs
    cases hKRs_conjugate
    dsimp only [id]
    rw [D.finiteReciprocityNaturalityFrobeniusConjugationLift_coe]
    refine Quotient.inductionOn' σ.1 ?_
    intro k
    rfl
  let S := D.frobeniusFixedField KR L hLK σ
  let Ss := D.frobeniusFixedField KRs
    (conjugateClosedSubgroup L s)
    (conjugateClosedSubgroup_mono hLK s) σs
  let hSK := D.frobeniusFixedField_le KR L hLK σ
  let hSsKs := D.frobeniusFixedField_le KRs
    (conjugateClosedSubgroup L s)
    (conjugateClosedSubgroup_mono hLK s) σs
  have hConjS : conjugateClosedSubgroup S s = Ss := by
    exact D.finiteReciprocityNaturalityFrobeniusFixedField_conjugate
      KR L hLK s σ
  let hSKfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field S hSK) :=
    D.frobeniusFixedField_finite KR L hLK σ
  let hConjSKfinite : Finite
      (Ks.field.toSubgroup ⧸
        extensionSubgroup Ks.field
          (conjugateClosedSubgroup S s)
          (conjugateClosedSubgroup_mono hSK s)) :=
    by
      change Finite
        ((conjugateClosedSubgroup K.field s).toSubgroup ⧸
          extensionSubgroup (conjugateClosedSubgroup K.field s)
            (conjugateClosedSubgroup S s)
            (conjugateClosedSubgroup_mono hSK s))
      exact finite_conjugateExtension K.field S hSK s
  let hSsKsfinite : Finite
      (Ks.field.toSubgroup ⧸ extensionSubgroup Ks.field Ss hSsKs) :=
    D.frobeniusFixedField_finite KRs
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s) σs
  let Sfinite : FiniteAbstractField G :=
    { field := S
      finite := D.frobeniusFixedField_absoluteFinite K L hLK σ }
  let Ssfinite : FiniteAbstractField G :=
    { field := Ss
      finite := D.frobeniusFixedField_absoluteFinite Ks
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s) σs }
  let π : ambientFixedAddSubgroup A S := v.chosenPrimeElement Sfinite
  have hπ : v.IsPrimeElement Sfinite π := v.chosenPrimeElement_isPrime Sfinite
  let πs0 : ambientFixedAddSubgroup A (conjugateClosedSubgroup S s) :=
    conjugateFixedElement A S s π
  have hπs0 : v.IsPrimeElement (Sfinite.conjugate s) πs0 := by
    change v.valuationAt (Sfinite.conjugate s) πs0 = v.oneValue
    rw [show v.valuationAt (Sfinite.conjugate s) πs0 =
        v.valuationAt Sfinite π by
      simpa [Sfinite, πs0] using
        v.normalizedValuation_conjugate Sfinite s π]
    exact hπ
  let πs : ambientFixedAddSubgroup A Ss := hConjS ▸ πs0
  have hπs : v.IsPrimeElement Ssfinite πs := by
    have htransport :=
      D.finiteReciprocityNaturality_isPrimeElement_transport v
        (Sfinite.conjugate s) Ssfinite (by exact hConjS) πs0 hπs0
    unfold πs
    exact htransport
  change finiteReciprocityNaturalityConjugationNormMap A K.field L hLK s
      (D.finiteReciprocityHom A v hAxiom K L hLK q) =
    D.finiteReciprocityHom A v hAxiom Ks
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s)
      ((finiteReciprocityNaturalityConjugation
        K.field L hLK s).toMonoidHom.toAdditive q)
  have hprimeNorm :
      finiteReciprocityNaturalityConjugationNormMap A K.field L hLK s
        (D.finiteReciprocityHom A v hAxiom K L hLK q) =
      finiteReciprocityNaturalityConjugationNormMap A K.field L hLK s
        (finiteNormClass A K.field L hLK
          (relativeNorm A K.field S hSK π)) := by
    rw [D.finiteReciprocityHom_apply_eq_primeNormClass
      A v hAxiom K L hLK q σ hσ π hπ]
  have hconjugateNorm :
      finiteReciprocityNaturalityConjugationNormMap A K.field L hLK s
        (finiteNormClass A K.field L hLK
          (relativeNorm A K.field S hSK π)) =
      finiteNormClass A Ks.field
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (relativeNorm A Ks.field
          (conjugateClosedSubgroup S s)
          (conjugateClosedSubgroup_mono hSK s) πs0) := by
    exact finiteReciprocityNaturality_conjugation_norm_class
      A K.field L S hLK hSK s π
  have htransportNorm :
      finiteNormClass A Ks.field
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (relativeNorm A Ks.field
          (conjugateClosedSubgroup S s)
          (conjugateClosedSubgroup_mono hSK s) πs0) =
      finiteNormClass A Ks.field
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (relativeNorm A Ks.field Ss hSsKs πs) := by
    apply congrArg (finiteNormClass A Ks.field
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s))
    have htransport :=
      finiteReciprocityNaturality_relativeNorm_right_transport A
        Ks.field (conjugateClosedSubgroup S s) Ss
        hConjS (conjugateClosedSubgroup_mono hSK s) hSsKs πs0
    simpa [πs] using htransport
  have hconjugatePrimeNorm :
      finiteNormClass A Ks.field
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        (relativeNorm A Ks.field Ss hSsKs πs) =
      D.finiteReciprocityHom A v hAxiom Ks
        (conjugateClosedSubgroup L s)
        (conjugateClosedSubgroup_mono hLK s)
        ((finiteReciprocityNaturalityConjugation
          K.field L hLK s).toMonoidHom.toAdditive q) := by
    rw [D.finiteReciprocityHom_apply_eq_primeNormClass
      A v hAxiom Ks
      (conjugateClosedSubgroup L s)
      (conjugateClosedSubgroup_mono hLK s)
      _ σs hσs πs hπs]
  exact hprimeNorm.trans (hconjugateNorm.trans (htransportNorm.trans hconjugatePrimeNorm))

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