Module

HerbrandFiniteness.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandFiniteness

14 declarations indexed from sourceView source ↗

Module documentation

Finiteness in the Herbrand exact hexagon

This file supplies the finiteness clause in Herbrand-quotient multiplicativity: for a short exact sequence of modules over a finite cyclic group, if the Herbrand quotients of any two terms are defined, then the quotient of the third term is defined as well.

Imports4

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Core
Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.TateComparison
Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Imported by8

def

HerbrandQuotientDefined

L38 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandQuotientDefined

Documentation

The condition that the Herbrand quotient of A is defined.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 HerbrandQuotientDefined (G : Type uG) (A : Type uA)
    [Group G] [Fintype G] [CommGroup A] [MulDistribMulAction G A]
    (σ : G) : Prop

theorem

finite_middle_of_exact

L45 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.finite_middle_of_exact

Documentation

In an exact pair X → Y → Z, finiteness of X and Z forces finiteness of Y.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 finite_middle_of_exact
    {X Y Z : Type}
    [Group X] [Group Y] [Group Z]
    (f : X →* Y) (g : Y →* Z) (hexact : MonoidHom.range f = MonoidHom.ker g)
    [Finite X] [Finite Z] :
    Finite Y

theorem

finite_middle_of_moduleCat_exact

L59 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.finite_middle_of_moduleCat_exact

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 finite_middle_of_moduleCat_exact
    {X Y Z : ModuleCat.{0} ℤ} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hexact : Function.Exact f g)
    [Finite X] [Finite Z] :
    Finite Y

def

tateHOneIsoHerbrandHMinusOne

L73 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.tateHOneIsoHerbrandHMinusOne

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 tateHOneIsoHerbrandHMinusOne
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) :
    tateCohomology (Rep.ofMulDistribMulAction G A) 1 ≅
      ModuleCat.of ℤ (Additive (HerbrandHMinusOne G A σ))

def

tateHMinusTwoIsoHerbrandH0

L87 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.tateHMinusTwoIsoHerbrandH0

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 tateHMinusTwoIsoHerbrandH0
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) :
    tateCohomology (Rep.ofMulDistribMulAction G A) (-2) ≅
      ModuleCat.of ℤ (Additive (HerbrandH0 G A))

theorem

herbrandQuotientDefined_middle_of_left_right

L104 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotientDefined_middle_of_left_right

Documentation

Herbrand-quotient multiplicativity, finiteness transfer from the first and third terms to the middle term.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 herbrandQuotientDefined_middle_of_left_right
    (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 : ∀ c : C, ∃ b : B, j b = c)
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    (hA : HerbrandQuotientDefined G A σ)
    (hC : HerbrandQuotientDefined G C σ) :
    HerbrandQuotientDefined G B σ

theorem

herbrandQuotientDefined_right_of_left_middle

L174 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotientDefined_right_of_left_middle

Documentation

Herbrand-quotient multiplicativity, finiteness transfer from the first and middle terms to the third term.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 herbrandQuotientDefined_right_of_left_middle
    (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 : ∀ c : C, ∃ b : B, j b = c)
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    (hA : HerbrandQuotientDefined G A σ)
    (hB : HerbrandQuotientDefined G B σ) :
    HerbrandQuotientDefined G C σ

theorem

herbrandQuotientDefined_left_of_middle_right

L248 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotientDefined_left_of_middle_right

Documentation

Herbrand-quotient multiplicativity, finiteness transfer from the middle and third terms to the first term.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 herbrandQuotientDefined_left_of_middle_right
    (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 : ∀ c : C, ∃ b : B, j b = c)
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    (hB : HerbrandQuotientDefined G B σ)
    (hC : HerbrandQuotientDefined G C σ) :
    HerbrandQuotientDefined G A σ

theorem

herbrandQuotientDefined_anyTwo

L321 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotientDefined_anyTwo

Documentation

Herbrand-quotient multiplicativity, the complete "any two imply the third" finiteness statement for a short exact sequence.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 herbrandQuotientDefined_anyTwo
    (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 : ∀ c : C, ∃ b : B, j b = c)
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) :
    (HerbrandQuotientDefined G A σ ∧ HerbrandQuotientDefined G B σ →
        HerbrandQuotientDefined G C σ) ∧
      (HerbrandQuotientDefined G A σ ∧ HerbrandQuotientDefined G C σ →
        HerbrandQuotientDefined G B σ) ∧
      (HerbrandQuotientDefined G B σ ∧ HerbrandQuotientDefined G C σ →
        HerbrandQuotientDefined G A σ)

theorem

herbrandQuotient_multiplicative_of_shortExact

L348 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_multiplicative_of_shortExact

Documentation

Herbrand-quotient multiplicativity, Herbrand-quotient multiplicativity once the three quotients are defined.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 herbrandQuotient_multiplicative_of_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 : ∀ c : C, ∃ b : B, j b = c)
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    [Finite (HerbrandH0 G A)] [Finite (HerbrandHMinusOne G A σ)]
    [Finite (HerbrandH0 G B)] [Finite (HerbrandHMinusOne G B σ)]
    [Finite (HerbrandH0 G C)] [Finite (HerbrandHMinusOne G C σ)] :
    herbrandQuotient (G := G) (A := B) σ =
      herbrandQuotient (G := G) (A := A) σ *
        herbrandQuotient (G := G) (A := C) σ

theorem

herbrandQuotient_multiplicative_of_left_right_defined

L368 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_multiplicative_of_left_right_defined

Documentation

Herbrand-quotient multiplicativity in its first two-defined form: if the quotients of A and C are defined, the quotient of B is defined and multiplicativity holds for that induced finiteness witness.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 herbrandQuotient_multiplicative_of_left_right_defined
    (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 : ∀ c : C, ∃ b : B, j b = c)
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    [Finite (HerbrandH0 G A)] [Finite (HerbrandHMinusOne G A σ)]
    [Finite (HerbrandH0 G C)] [Finite (HerbrandHMinusOne G C σ)] :
    ∃ hB : HerbrandQuotientDefined G B σ,
      @herbrandQuotient G B _ _ _ _ σ hB.1 hB.2 =
        herbrandQuotient (G := G) (A := A) σ *
          herbrandQuotient (G := G) (A := C) σ

theorem

herbrandQuotient_multiplicative_of_left_middle_defined

L395 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_multiplicative_of_left_middle_defined

Documentation

Herbrand-quotient multiplicativity in its second two-defined form: if the quotients of A and B are defined, the quotient of C is defined and multiplicativity holds for that induced finiteness witness.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 herbrandQuotient_multiplicative_of_left_middle_defined
    (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 : ∀ c : C, ∃ b : B, j b = c)
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    [Finite (HerbrandH0 G A)] [Finite (HerbrandHMinusOne G A σ)]
    [Finite (HerbrandH0 G B)] [Finite (HerbrandHMinusOne G B σ)] :
    ∃ hC : HerbrandQuotientDefined G C σ,
      herbrandQuotient (G := G) (A := B) σ =
        herbrandQuotient (G := G) (A := A) σ *
          @herbrandQuotient G C _ _ _ _ σ hC.1 hC.2

theorem

herbrandQuotient_multiplicative_of_middle_right_defined

L422 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_multiplicative_of_middle_right_defined

Documentation

Herbrand-quotient multiplicativity in its third two-defined form: if the quotients of B and C are defined, the quotient of A is defined and multiplicativity holds for that induced finiteness witness.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 herbrandQuotient_multiplicative_of_middle_right_defined
    (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 : ∀ c : C, ∃ b : B, j b = c)
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    [Finite (HerbrandH0 G B)] [Finite (HerbrandHMinusOne G B σ)]
    [Finite (HerbrandH0 G C)] [Finite (HerbrandHMinusOne G C σ)] :
    ∃ hA : HerbrandQuotientDefined G A σ,
      herbrandQuotient (G := G) (A := B) σ =
        @herbrandQuotient G A _ _ _ _ σ hA.1 hA.2 *
          herbrandQuotient (G := G) (A := C) σ

theorem

herbrandQuotient_eq_one_of_finite_module

L447 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_eq_one_of_finite_module

Documentation

Herbrand-quotient multiplicativity, the finite-module case.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
universe uG uA
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 herbrandQuotient_eq_one_of_finite_module
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) [Finite A] :
    herbrandQuotient (G := G) (A := A) σ = 1

Module documentation

Finiteness in the Herbrand exact hexagon

Declarations