NYLL
Module

TateTransport.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.TateTransport
10 declarations indexed from sourceView source ↗

Module documentation

The local class-field-axiom theorem: transport of cyclic Tate complexes

The fixed-field realization of an abstract extension changes both the presentation of its cyclic group and the presentation of its coefficient module. This file records the two honest functorial comparisons needed to transport the local class-field-axiom theorem: reindexing a representation along a group isomorphism and replacing a representation by an isomorphic one.

Imports1
Imported by3

Declarations

theorem

map_cyclicGenerator

L34 ↗
LocalClassFieldTheory.map_cyclicGenerator
Documentation

A generator remains a generator after applying a group isomorphism.

Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section CyclicGenerator
variable {Q P : Type} [Group Q] [Group P]
Lean source · statement
theorem map_cyclicGenerator (e : Q ≃* P) (g : Q)
    (hg : ∀ q : Q, q ∈ Subgroup.zpowers g) :
    ∀ p : P, p ∈ Subgroup.zpowers (e g)
theorem

res_norm_eq

L50 ↗
LocalClassFieldTheory.res_norm_eq
Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section GroupEquiv
variable {R Q P : Type} [CommRing R]
  [CommGroup Q] [CommGroup P] [Fintype Q] [Fintype P]
Lean source · full declaration
theorem res_norm_eq (e : Q ≃* P) (A : Rep R P) :
    let Ares : Rep R Q :=
      Rep.res e.toMonoidHom A
    ModuleCat.ofHom Ares.norm.hom.toLinearMap =
      ModuleCat.ofHom A.norm.hom.toLinearMap := by
  let Ares : Rep R Q :=
    Rep.res e.toMonoidHom A
  apply congrArg ModuleCat.ofHom
  change Representation.norm Ares.ρ = Representation.norm A.ρ
  simp only [Representation.norm]
  exact Fintype.sum_equiv e.toEquiv
    (fun q : Q => Ares.ρ q)
    (fun p : P => A.ρ p) (fun _ => rfl)
def

normHomCompSubResEquivIso

L66 ↗
LocalClassFieldTheory.normHomCompSubResEquivIso
Documentation

Reindexing along a group isomorphism preserves the cyclic H⁰ short complex.

Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section GroupEquiv
variable {R Q P : Type} [CommRing R]
  [CommGroup Q] [CommGroup P] [Fintype Q] [Fintype P]
Lean source · statement
def normHomCompSubResEquivIso
    (e : Q ≃* P) (A : Rep R P) (g : Q) :
    Rep.FiniteCyclicGroup.normHomCompSub
        (Rep.res e.toMonoidHom A) g ≅
      Rep.FiniteCyclicGroup.normHomCompSub A (e g)
def

subCompNormHomResEquivIso

L80 ↗
LocalClassFieldTheory.subCompNormHomResEquivIso
Documentation

Reindexing along a group isomorphism preserves the cyclic H⁻¹ short complex.

Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section GroupEquiv
variable {R Q P : Type} [CommRing R]
  [CommGroup Q] [CommGroup P] [Fintype Q] [Fintype P]
Lean source · statement
def subCompNormHomResEquivIso
    (e : Q ≃* P) (A : Rep R P) (g : Q) :
    Rep.FiniteCyclicGroup.subCompNormHom
        (Rep.res e.toMonoidHom A) g ≅
      Rep.FiniteCyclicGroup.subCompNormHom A (e g)
def

normHomCompSubHomologyResEquivIso

L93 ↗
LocalClassFieldTheory.normHomCompSubHomologyResEquivIso
Documentation

Homology-level group-reindexing comparison in degree zero.

Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section GroupEquiv
variable {R Q P : Type} [CommRing R]
  [CommGroup Q] [CommGroup P] [Fintype Q] [Fintype P]
Lean source · statement
def normHomCompSubHomologyResEquivIso
    (e : Q ≃* P) (A : Rep R P) (g : Q) :
    (Rep.FiniteCyclicGroup.normHomCompSub
        (Rep.res e.toMonoidHom A) g).homology ≅
      (Rep.FiniteCyclicGroup.normHomCompSub A (e g)).homology
def

subCompNormHomHomologyResEquivIso

L101 ↗
LocalClassFieldTheory.subCompNormHomHomologyResEquivIso
Documentation

Homology-level group-reindexing comparison in degree minus one.

Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section GroupEquiv
variable {R Q P : Type} [CommRing R]
  [CommGroup Q] [CommGroup P] [Fintype Q] [Fintype P]
Lean source · statement
def subCompNormHomHomologyResEquivIso
    (e : Q ≃* P) (A : Rep R P) (g : Q) :
    (Rep.FiniteCyclicGroup.subCompNormHom
        (Rep.res e.toMonoidHom A) g).homology ≅
      (Rep.FiniteCyclicGroup.subCompNormHom A (e g)).homology
def

normHomCompSubIsoOfRepIso

L116 ↗
LocalClassFieldTheory.normHomCompSubIsoOfRepIso
Documentation

Isomorphic representations have isomorphic cyclic H⁰ short complexes.

Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section RepresentationIso
variable {R Q : Type} [CommRing R] [CommGroup Q] [Fintype Q]
Lean source · statement
def normHomCompSubIsoOfRepIso
    {M N : Rep R Q} (e : M ≅ N) (g : Q) :
    Rep.FiniteCyclicGroup.normHomCompSub M g ≅
      Rep.FiniteCyclicGroup.normHomCompSub N g
def

subCompNormHomIsoOfRepIso

L139 ↗
LocalClassFieldTheory.subCompNormHomIsoOfRepIso
Documentation

Isomorphic representations have isomorphic cyclic H⁻¹ short complexes.

Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section RepresentationIso
variable {R Q : Type} [CommRing R] [CommGroup Q] [Fintype Q]
Lean source · statement
def subCompNormHomIsoOfRepIso
    {M N : Rep R Q} (e : M ≅ N) (g : Q) :
    Rep.FiniteCyclicGroup.subCompNormHom M g ≅
      Rep.FiniteCyclicGroup.subCompNormHom N g
def

normHomCompSubHomologyIsoOfRepIso

L161 ↗
LocalClassFieldTheory.normHomCompSubHomologyIsoOfRepIso
Documentation

Homology-level representation-isomorphism comparison in degree zero.

Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section RepresentationIso
variable {R Q : Type} [CommRing R] [CommGroup Q] [Fintype Q]
Lean source · statement
def normHomCompSubHomologyIsoOfRepIso
    {M N : Rep R Q} (e : M ≅ N) (g : Q) :
    (Rep.FiniteCyclicGroup.normHomCompSub M g).homology ≅
      (Rep.FiniteCyclicGroup.normHomCompSub N g).homology
def

subCompNormHomHomologyIsoOfRepIso

L169 ↗
LocalClassFieldTheory.subCompNormHomHomologyIsoOfRepIso
Documentation

Homology-level representation-isomorphism comparison in degree minus one.

Source context 6 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
open CategoryTheory
section RepresentationIso
variable {R Q : Type} [CommRing R] [CommGroup Q] [Fintype Q]
Lean source · statement
def subCompNormHomHomologyIsoOfRepIso
    {M N : Rep R Q} (e : M ≅ N) (g : Q) :
    (Rep.FiniteCyclicGroup.subCompNormHom M g).homology ≅
      (Rep.FiniteCyclicGroup.subCompNormHom N g).homology

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