Module

MainTransferFrobeniusGeometry.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.MainTransferFrobeniusGeometry

17 declarations indexed from sourceView source ↗

Module documentation

Transfer--norm Frobenius geometry

For a finite Galois extension and an intermediate field, this module builds the Frobenius-side subgroup and orbit equivalences used in transfer--norm naturality. The reusable orbit and double-coset constructions are isolated in DoubleCosetOrbitGeometry.

Imports2

Imported by2

def

transferNormNaturalityIntermediateAbsoluteEquiv

L40 ↗

ClassFormation.transferNormNaturalityIntermediateAbsoluteEquiv

Documentation

The absolute group of an intermediate field, identified with its literal copy inside the absolute group of the base field.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

def transferNormNaturalityIntermediateAbsoluteEquiv
    (K K' : ClosedSubgroup G)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup) :
    K'.toSubgroup ≃* extensionSubgroup K K' hK'K

theorem

transferNormNaturalityIntermediateAbsoluteEquiv_apply

L54 ↗

ClassFormation.transferNormNaturalityIntermediateAbsoluteEquiv_apply

Documentation

The absolute intermediate-field equivalence evaluates by the underlying transfer map.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem transferNormNaturalityIntermediateAbsoluteEquiv_apply
    (K K' : ClosedSubgroup G)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    (k' : K'.toSubgroup) :
    ((transferNormNaturalityIntermediateAbsoluteEquiv K K' hK'K k').1 : G) = k'.1

theorem

transferNormNaturality_intermediateExtension_normal

L62 ↗

ClassFormation.transferNormNaturality_intermediateExtension_normal

Documentation

Normality of L | K restricts to every intermediate field 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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem transferNormNaturality_intermediateExtension_normal
    (K K' L : ClosedSubgroup G)
    (hLK' : L.toSubgroup ≤ K'.toSubgroup)
    (hK'K : K'.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L (hLK'.trans hK'K)).Normal] :
    (extensionSubgroup K' L hLK').Normal

theorem

transferNormNaturalityFrobeniusTowerMap_injective

L82 ↗

ClassFormation.DegreeData.transferNormNaturalityFrobeniusTowerMap_injective

Documentation

The restriction map on the infinite Frobenius quotients is injective when the top field is unchanged.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityFrobeniusTowerMap_injective
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal] :
    Function.Injective
      (D.finiteReciprocityNaturalityFrobeniusTowerMap
        E.base.field E.field.field L L
        (hL.trans E.below) hL E.below le_rfl)

def

transferNormNaturalityFrobeniusIntermediateSubgroup

L119 ↗

ClassFormation.DegreeData.transferNormNaturalityFrobeniusIntermediateSubgroup

Documentation

The copy of G(\widetilde L/K') inside G(\widetilde L/K). This is the subgroup H used in the classical double-coset proof of transfer--norm naturality.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def transferNormNaturalityFrobeniusIntermediateSubgroup
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal] :
    Subgroup (E.base.field.toSubgroup ⧸
      D.extensionInertiaWithin E.base.field L (hL.trans E.below))

theorem

transferNormNaturalityFrobeniusIntermediateSubgroup_eq_map

L134 ↗

ClassFormation.DegreeData.transferNormNaturalityFrobeniusIntermediateSubgroup_eq_map

Documentation

The subgroup above is also the image of G_K' under the quotient projection G_K → G(\widetilde L/K).

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityFrobeniusIntermediateSubgroup_eq_map
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal] :
    D.transferNormNaturalityFrobeniusIntermediateSubgroup E L hL =
      (extensionSubgroup E.base.field E.field.field E.below).map
        (QuotientGroup.mk'
          (D.extensionInertiaWithin E.base.field L
            (hL.trans E.below)))

def

transferNormNaturalityIntermediateToFrobeniusSubgroup

L162 ↗

ClassFormation.DegreeData.transferNormNaturalityIntermediateToFrobeniusSubgroup

Documentation

Quotient projection maps the literal absolute subgroup belonging to K' onto its copy H inside G(\widetilde L/K).

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def transferNormNaturalityIntermediateToFrobeniusSubgroup
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal] :
    extensionSubgroup E.base.field E.field.field E.below →*
      D.transferNormNaturalityFrobeniusIntermediateSubgroup E L hL

theorem

transferNormNaturalityIntermediateToFrobeniusSubgroup_surjective

L183 ↗

ClassFormation.DegreeData.transferNormNaturalityIntermediateToFrobeniusSubgroup_surjective

Documentation

The map from the intermediate quotient onto the Frobenius subgroup is surjective.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityIntermediateToFrobeniusSubgroup_surjective
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal] :
    Function.Surjective
      (D.transferNormNaturalityIntermediateToFrobeniusSubgroup
        E L hL)

theorem

transferNormNaturalityIntermediateToFrobeniusSubgroup_apply

L210 ↗

ClassFormation.DegreeData.transferNormNaturalityIntermediateToFrobeniusSubgroup_apply

Documentation

The intermediate-to-Frobenius map has the stated value on each representative.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityIntermediateToFrobeniusSubgroup_apply
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal]
    (m : extensionSubgroup E.base.field E.field.field E.below) :
    (D.transferNormNaturalityIntermediateToFrobeniusSubgroup
      E L hL m).1 =
        (QuotientGroup.mk m.1 : E.base.field.toSubgroup ⧸
          D.extensionInertiaWithin E.base.field L (hL.trans E.below))

theorem

frobeniusFixedCosetClosureEquiv_equivariant

L226 ↗

ClassFormation.DegreeData.frobeniusFixedCosetClosureEquiv_equivariant

Documentation

The canonical coset equivalence from G_K/G_Σ to G(\widetilde L/K)/Γ intertwines the two copies of the K'-action.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem frobeniusFixedCosetClosureEquiv_equivariant
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal]
    (σ : D.FrobeniusElements E.base L (hL.trans E.below))
    (m : extensionSubgroup E.base.field E.field.field E.below)
    (x : E.base.field.toSubgroup ⧸ extensionSubgroup E.base.field
      (D.frobeniusFixedField E.base L (hL.trans E.below) σ)
      (D.frobeniusFixedField_le E.base L (hL.trans E.below) σ)) :
    D.frobeniusFixedCosetClosureEquiv E.base L (hL.trans E.below) σ (m • x) =
      (D.transferNormNaturalityIntermediateToFrobeniusSubgroup
        E L hL m) •
        D.frobeniusFixedCosetClosureEquiv E.base L
          (hL.trans E.below) σ x

theorem

transferNormNaturalityExtensionRestriction_surjective

L254 ↗

ClassFormation.DegreeData.transferNormNaturalityExtensionRestriction_surjective

Documentation

Restriction from the infinite Frobenius quotient onto the finite Galois quotient is surjective.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityExtensionRestriction_surjective
    (D : DegreeData G)
    (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hLnormal : (extensionSubgroup K L hLK).Normal] :
    Function.Surjective (D.extensionRestriction K L hLK)

theorem

transferNormNaturalityExtensionRestriction_ker_le_intermediate

L267 ↗

ClassFormation.DegreeData.transferNormNaturalityExtensionRestriction_ker_le_intermediate

Documentation

The kernel of restriction to G(L/K) is contained in the subgroup coming from G(\widetilde L/K').

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityExtensionRestriction_ker_le_intermediate
    (D : DegreeData G) [IsTopologicalGroup G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal] :
    (D.extensionRestriction E.base.field L (hL.trans E.below)).ker ≤
      D.transferNormNaturalityFrobeniusIntermediateSubgroup E L hL

theorem

transferNormNaturalityFrobeniusIntermediateFiniteIndex

L298 ↗

ClassFormation.DegreeData.transferNormNaturalityFrobeniusIntermediateFiniteIndex

Documentation

H has finite index in G(\widetilde L/K), with no normality assumption on the intermediate extension K'/K.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityFrobeniusIntermediateFiniteIndex
    (D : DegreeData G) [IsTopologicalGroup G]
    (R : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ R.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup R.base.field L (hL.trans R.below)).Normal]
    [hL'normal : (extensionSubgroup R.field.field L hL).Normal] :
    (D.transferNormNaturalityFrobeniusIntermediateSubgroup R L hL).FiniteIndex

theorem

transferNormNaturalityFrobeniusIntermediate_isClosed

L326 ↗

ClassFormation.DegreeData.transferNormNaturalityFrobeniusIntermediate_isClosed

Documentation

The copy of G(\widetilde L/K') is closed in G(\widetilde L/K).

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityFrobeniusIntermediate_isClosed
    (D : DegreeData G) [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal] :
    IsClosed (D.transferNormNaturalityFrobeniusIntermediateSubgroup
      E L hL : Set
        (E.base.field.toSubgroup ⧸ D.extensionInertiaWithin E.base.field L
          (hL.trans E.below)))

def

transferNormNaturalityTransferNormOrbitEquiv

L362 ↗

ClassFormation.DegreeData.transferNormNaturalityTransferNormOrbitEquiv

Documentation

The transfer-orbit index set ⟨σ⟩ \ G(\widetilde L/K) / H is canonically the norm double-coset index set G_K' \ G_K / G_Σ. The equivalence is inversion of double cosets, followed by passage from powers of σ to their closure Γ and the canonical identification G_K/G_Σ ≃ G(\widetilde L/K)/Γ.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def transferNormNaturalityTransferNormOrbitEquiv
    (D : DegreeData G) [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal]
    (σ : D.FrobeniusElements E.base L (hL.trans E.below)) :
    Quotient (orbitRel (Subgroup.zpowers σ.1)
      ((E.base.field.toSubgroup ⧸ D.extensionInertiaWithin E.base.field L
        (hL.trans E.below)) ⧸
          D.transferNormNaturalityFrobeniusIntermediateSubgroup
            E L hL)) ≃
      Quotient (orbitRel
        (extensionSubgroup E.base.field E.field.field E.below)
        (E.base.field.toSubgroup ⧸ extensionSubgroup E.base.field
          (D.frobeniusFixedField E.base L (hL.trans E.below) σ)
          (D.frobeniusFixedField_le E.base L
            (hL.trans E.below) σ)))

theorem

transferNormNaturalityTransferNormOrbitEquiv_mk

L424 ↗

ClassFormation.DegreeData.transferNormNaturalityTransferNormOrbitEquiv_mk

Documentation

The transfer-norm orbit equivalence sends quotient representatives to their norm orbits.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityTransferNormOrbitEquiv_mk
    (D : DegreeData G) [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal]
    (σ : D.FrobeniusElements E.base L (hL.trans E.below))
    (k : E.base.field.toSubgroup) :
    D.transferNormNaturalityTransferNormOrbitEquiv E L hL σ
        (Quotient.mk'' (QuotientGroup.mk
          (QuotientGroup.mk k : E.base.field.toSubgroup ⧸
            D.extensionInertiaWithin E.base.field L (hL.trans E.below)) :
          (E.base.field.toSubgroup ⧸ D.extensionInertiaWithin E.base.field L
            (hL.trans E.below)) ⧸
              D.transferNormNaturalityFrobeniusIntermediateSubgroup
                E L hL)) =
      Quotient.mk'' (QuotientGroup.mk k⁻¹ :
        E.base.field.toSubgroup ⧸ extensionSubgroup E.base.field
          (D.frobeniusFixedField E.base L (hL.trans E.below) σ)
          (D.frobeniusFixedField_le E.base L
            (hL.trans E.below) σ))

theorem

transferNormNaturalityTransferNormOrbitEquiv_apply

L458 ↗

ClassFormation.DegreeData.transferNormNaturalityTransferNormOrbitEquiv_apply

Documentation

On the classical chosen transfer representative t, the preceding equivalence is literally the norm orbit represented by t⁻¹.

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
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem transferNormNaturalityTransferNormOrbitEquiv_apply
    (D : DegreeData G) [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (E : FiniteResidueAbstractExtension D) (L : ClosedSubgroup G)
    (hL : L.toSubgroup ≤ E.field.field.toSubgroup)
    [hLnormal :
      (extensionSubgroup E.base.field L (hL.trans E.below)).Normal]
    [hL'normal : (extensionSubgroup E.field.field L hL).Normal]
    (σ : D.FrobeniusElements E.base L (hL.trans E.below))
    (q : Quotient (orbitRel (Subgroup.zpowers σ.1)
      ((E.base.field.toSubgroup ⧸ D.extensionInertiaWithin E.base.field L
        (hL.trans E.below)) ⧸
          D.transferNormNaturalityFrobeniusIntermediateSubgroup
            E L hL))) :
    D.transferNormNaturalityTransferNormOrbitEquiv E L hL σ q =
      Quotient.mk'' (QuotientGroup.mk (Quotient.out q.out.out)⁻¹ :
        E.base.field.toSubgroup ⧸ extensionSubgroup E.base.field
          (D.frobeniusFixedField E.base L (hL.trans E.below) σ)
          (D.frobeniusFixedField_le E.base L
            (hL.trans E.below) σ))

Module documentation

Transfer--norm Frobenius geometry

Declarations