Module

TateComparison.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.TateComparison

12 declarations indexed from sourceView source ↗

Module documentation

Comparisons between arithmetic Herbrand quotient presentations and mathlib Tate cohomology.

Imports2

Imported by9

theorem

repExact_of_hom_exact

L20 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.repExact_of_hom_exact

Source context 4 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w

Lean source · statement

theorem repExact_of_hom_exact {k G : Type u} [CommRing k] [Group G]
    (S : ShortComplex (Rep.{w} k G))
    (h : ∀ b : S.X₂, S.g.hom b = 0 → ∃ a : S.X₁, S.f.hom a = b) :
    S.Exact

def

equivariantRepHom

L34 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.equivariantRepHom

Documentation

An equivariant homomorphism of multiplicative G-modules, regarded as the corresponding morphism between mathlib's additive ℤ-representations.

Source context 7 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

def equivariantRepHom (f : A →* B)
    (hf : ∀ (g : G) (a : A), f (g • a) = g • f a) :
    Rep.ofMulDistribMulAction G A ⟶ Rep.ofMulDistribMulAction G B

theorem

equivariantRepHom_apply

L47 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.equivariantRepHom_apply

Source context 8 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
omit [Fintype G] in

Lean source · statement

theorem equivariantRepHom_apply (f : A →* B)
    (hf : ∀ (g : G) (a : A), f (g • a) = g • f a) (a : Additive A) :
    equivariantRepHom f hf a = Additive.ofMul (f a.toMul)

def

equivariantShortComplex

L54 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.equivariantShortComplex

Documentation

The short complex of mathlib representations associated to two equivariant multiplicative homomorphisms whose composite is trivial.

Source context 7 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

def equivariantShortComplex
    (i : A →* B) (j : B →* C)
    (hi : ∀ (g : G) (a : A), i (g • a) = g • i a)
    (hj : ∀ (g : G) (b : B), j (g • b) = g • j b)
    (hker : ∀ b : B, j b = 1 ↔ ∃ a : A, i a = b) :
    ShortComplex (Rep ℤ G)

theorem

equivariantShortComplex_shortExact

L68 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.equivariantShortComplex_shortExact

Source context 8 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
omit [Fintype G] in

Lean source · statement

theorem equivariantShortComplex_shortExact
    (i : A →* B) (j : B →* C)
    (hi : ∀ (g : G) (a : A), i (g • a) = g • i a)
    (hj : ∀ (g : G) (b : B), j (g • b) = g • j b)
    (hker : ∀ b : B, j b = 1 ↔ ∃ a : A, i a = b)
    (hinj : Function.Injective i) (hsurj : Function.Surjective j) :
    (equivariantShortComplex i j hi hj hker).ShortExact

theorem

repNorm_toMul

L99 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.repNorm_toMul

Source context 7 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

theorem repNorm_toMul (a : Additive A) :
    Additive.toMul
        ((Rep.ofMulDistribMulAction G A).ρ.norm a) =
      tateNorm G A a.toMul

theorem

repSigmaMinusOne_toMul

L109 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.repSigmaMinusOne_toMul

Source context 7 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

theorem repSigmaMinusOne_toMul
    {G A : Type} [CommGroup G] [CommGroup A]
    [MulDistribMulAction G A] (σ : G) (a : Additive A) :
    Additive.toMul
        ((Rep.toAdditive (M := G) (G := A))
          (((Rep.ofMulDistribMulAction G A).applyAsHom σ -
            𝟙 (Rep.ofMulDistribMulAction G A)).hom a)) =
      sigmaMinusOne G A σ a.toMul

def

fixedCyclesAddEquiv

L146 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.fixedCyclesAddEquiv

Source context 7 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · full declaration

def fixedCyclesAddEquiv :
    LinearMap.ker
        (groupCohomology.d₀₁ (Rep.ofMulDistribMulAction G A)).hom ≃+
      Additive (fixedSubgroup G A) where
  toFun x :=
    Additive.ofMul
      ⟨x.1.toMul, by
        have hx : x.1 ∈ (Rep.ofMulDistribMulAction G A).ρ.invariants := by
          rw [← groupCohomology.d₀₁_ker_eq_invariants]
          exact x.2
        intro g
        apply Additive.ofMul.injective
        exact hx g⟩
  invFun x :=
    ⟨Additive.ofMul x.toMul.1, by
      rw [groupCohomology.d₀₁_ker_eq_invariants]
      intro g
      apply Additive.ofMul.injective
      exact x.toMul.2 g⟩
  left_inv x := by
    apply Subtype.ext
    rfl
  right_inv x := by
    apply Additive.ofMul.injective
    apply Subtype.ext
    rfl
  map_add' x y := by
    apply Additive.ofMul.injective
    apply Subtype.ext
    rfl

def

tateH0IsoHerbrandH0

L179 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.tateH0IsoHerbrandH0

Documentation

Mathlib's degree-zero Tate cohomology is the arithmetic fixed-point quotient by the norm image used by HerbrandH0.

Source context 7 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

def tateH0IsoHerbrandH0 :
    tateCohomology (Rep.ofMulDistribMulAction G A) 0 ≅
      ModuleCat.of ℤ (Additive (HerbrandH0 G A))

def

normKernelCyclesAddEquiv

L246 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.normKernelCyclesAddEquiv

Source context 7 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · full declaration

def normKernelCyclesAddEquiv :
    LinearMap.ker
        (Rep.ofMulDistribMulAction G A).norm.toModuleCatHom.hom ≃+
      Additive (normKernelSubgroup G A) where
  toFun x :=
    let a : Additive A := x.1
    Additive.ofMul
      ⟨a.toMul, by
        change tateNorm G A a.toMul = 1
        have hx := x.2
        change (Rep.ofMulDistribMulAction G A).ρ.norm a = 0 at hx
        exact (repNorm_toMul (G := G) (A := A) a).symm.trans <| by
          rw [hx]
          rfl⟩
  invFun x :=
    let a : Additive A := Additive.ofMul x.toMul.1
    ⟨a, by
      have hx0 := x.toMul.2
      change tateNorm G A x.toMul.1 = 1 at hx0
      have hx : tateNorm G A a.toMul = 1 := hx0
      change (Rep.ofMulDistribMulAction G A).ρ.norm a = 0
      unfold Rep.ofMulDistribMulAction
      apply Additive.toMul.injective
      change Additive.toMul
          ((Representation.ofMulDistribMulAction G A).norm a) = (1 : A)
      exact
        (Representation.norm_ofMulDistribMulAction_eq
          (G := G) (M := A) a).trans <| by
            simpa [tateNorm] using hx⟩
  left_inv x := by
    apply Subtype.ext
    rfl
  right_inv x := by
    apply Additive.ofMul.injective
    apply Subtype.ext
    rfl
  map_add' x y := by
    apply Additive.ofMul.injective
    apply Subtype.ext
    rfl

def

tateHMinusOneIsoHerbrandHMinusOne_of_commGroup

L287 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.tateHMinusOneIsoHerbrandHMinusOne_of_commGroup

Source context 7 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

def tateHMinusOneIsoHerbrandHMinusOne_of_commGroup
    {G A : Type} [CommGroup G] [Fintype G] [CommGroup A]
    [MulDistribMulAction G A]
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) :
    tateCohomology (Rep.ofMulDistribMulAction G A) (-1) ≅
      ModuleCat.of ℤ (Additive (HerbrandHMinusOne G A σ))

def

tateHMinusOneIsoHerbrandHMinusOne

L352 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.tateHMinusOneIsoHerbrandHMinusOne

Documentation

For a chosen generator σ, mathlib's degree-minus-one Tate cohomology is the arithmetic quotient ker N / im (σ - 1) used by HerbrandHMinusOne.

Source context 7 commands

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

open CategoryTheory
namespace CyclicCohomology.ProfiniteCohomology.Herbrand
noncomputable section
universe u w
variable {G A B C : Type}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]

Lean source · statement

def tateHMinusOneIsoHerbrandHMinusOne
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) :
    tateCohomology (Rep.ofMulDistribMulAction G A) (-1) ≅
      ModuleCat.of ℤ (Additive (HerbrandHMinusOne G A σ))

Module documentation

Declarations