NYLL
Module

BinaryProduct.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.BinaryProduct
15 declarations indexed from sourceView source ↗

Module documentation

Low-degree Tate cohomology of binary products

This specializes the dependent-product calculation to two possibly different coefficient groups. It is used to join the unrestricted and integral parts of a supported idele group.

Imports3
Imported by2

Declarations

abbrev

BinaryCoefficientFamily

L35 ↗
CyclicCohomology.BinaryCoefficientFamily
Documentation

The two-element dependent family associated with A × B.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · full declaration
abbrev BinaryCoefficientFamily : Bool → Type uA
  | false => A
  | true => B
instance

binaryCoefficientFamilyCommGroup

L39 ↗
CyclicCohomology.binaryCoefficientFamilyCommGroup
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · full declaration
instance binaryCoefficientFamilyCommGroup :
    ∀ i, CommGroup (BinaryCoefficientFamily A B i)
  | false => inferInstance
  | true => inferInstance
def

binaryCoefficientFamilyAction

L46 ↗
CyclicCohomology.binaryCoefficientFamilyAction
Documentation

The componentwise G-action on the binary coefficient family.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · full declaration
def binaryCoefficientFamilyAction :
    ∀ i, MulDistribMulAction G
      (BinaryCoefficientFamily A B i)
  | false => inferInstance
  | true => inferInstance
instance

(anonymous instance)

L52 ↗
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · statement
instance
    (i : Bool) :
    MulDistribMulAction G
      (BinaryCoefficientFamily A B i)
def

prodEquivBinaryCoefficientFamily

L59 ↗
CyclicCohomology.prodEquivBinaryCoefficientFamily
Documentation

Reindex a binary product as a dependent family over Bool.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · full declaration
def prodEquivBinaryCoefficientFamily :
    A × B ≃* ∀ i, BinaryCoefficientFamily A B i where
  toFun x
    | false => x.1
    | true => x.2
  invFun x := ⟨x false, x true⟩
  left_inv _ := rfl
  right_inv x := by
    funext i
    cases i <;> rfl
  map_mul' _ _ := by
    funext i
    cases i <;> rfl
theorem

prodEquivBinaryCoefficientFamily_smul

L76 ↗
CyclicCohomology.prodEquivBinaryCoefficientFamily_smul
Documentation

The binary reindexing is equivariant for the componentwise actions.

Source context 9 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
omit [Fintype G] in
Lean source · full declaration
theorem prodEquivBinaryCoefficientFamily_smul
    (g : G) (x : A × B) :
    letI : ∀ i, MulDistribMulAction G
        (BinaryCoefficientFamily A B i) :=
      binaryCoefficientFamilyAction A B
    letI : MulDistribMulAction G
        (∀ i, BinaryCoefficientFamily A B i) :=
      piMulDistribMulAction G
        (BinaryCoefficientFamily A B)
    prodEquivBinaryCoefficientFamily A B (g • x) =
      g • prodEquivBinaryCoefficientFamily A B x := by
  funext i
  cases i <;> rfl
def

piHerbrandH0EquivProd

L90 ↗
CyclicCohomology.piHerbrandH0EquivProd
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · full declaration
def piHerbrandH0EquivProd :
    (∀ i, HerbrandH0 G
      (BinaryCoefficientFamily A B i)) ≃*
        HerbrandH0 G A × HerbrandH0 G B where
  toFun x := ⟨x false, x true⟩
  invFun x
    | false => x.1
    | true => x.2
  left_inv x := by
    funext i
    cases i <;> rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
def

piHerbrandHMinusOneEquivProd

L104 ↗
CyclicCohomology.piHerbrandHMinusOneEquivProd
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · full declaration
def piHerbrandHMinusOneEquivProd
    (σ : G) :
    (∀ i, HerbrandHMinusOne G
      (BinaryCoefficientFamily A B i) σ) ≃*
        HerbrandHMinusOne G A σ ×
          HerbrandHMinusOne G B σ where
  toFun x := ⟨x false, x true⟩
  invFun x
    | false => x.1
    | true => x.2
  left_inv x := by
    funext i
    cases i <;> rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
def

herbrandH0ProdEquiv

L121 ↗
CyclicCohomology.herbrandH0ProdEquiv
Documentation

Degree-zero Tate cohomology commutes with a binary product.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · statement
def herbrandH0ProdEquiv :
    HerbrandH0 G (A × B) ≃*
      HerbrandH0 G A × HerbrandH0 G B
def

herbrandHMinusOneProdEquiv

L140 ↗
CyclicCohomology.herbrandHMinusOneProdEquiv
Documentation

Degree-minus-one Tate cohomology commutes with a binary product.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · statement
def herbrandHMinusOneProdEquiv
    (σ : G) :
    HerbrandHMinusOne G (A × B) σ ≃*
      HerbrandHMinusOne G A σ ×
        HerbrandHMinusOne G B σ
theorem

herbrandH0ProdFinite

L161 ↗
CyclicCohomology.herbrandH0ProdFinite
Documentation

Finiteness of degree zero is preserved by a binary product.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · statement
theorem herbrandH0ProdFinite
    [Finite (HerbrandH0 G A)]
    [Finite (HerbrandH0 G B)] :
    Finite (HerbrandH0 G (A × B))
theorem

herbrandHMinusOneProdFinite

L170 ↗
CyclicCohomology.herbrandHMinusOneProdFinite
Documentation

Finiteness of degree minus one is preserved by a binary product.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · statement
theorem herbrandHMinusOneProdFinite
    (σ : G)
    [Finite (HerbrandHMinusOne G A σ)]
    [Finite (HerbrandHMinusOne G B σ)] :
    Finite (HerbrandHMinusOne G (A × B) σ)
theorem

herbrandH0Prod_card

L181 ↗
CyclicCohomology.herbrandH0Prod_card
Documentation

Cardinality of degree-zero Tate cohomology for a binary product.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · full declaration
theorem herbrandH0Prod_card
    [Finite (HerbrandH0 G A)]
    [Finite (HerbrandH0 G B)] :
    letI : Finite (HerbrandH0 G (A × B)) :=
      herbrandH0ProdFinite A B
    Nat.card (HerbrandH0 G (A × B)) =
      Nat.card (HerbrandH0 G A) *
        Nat.card (HerbrandH0 G B) := by
  rw [Nat.card_congr (herbrandH0ProdEquiv A B).toEquiv,
    Nat.card_prod]
theorem

herbrandHMinusOneProd_card

L194 ↗
CyclicCohomology.herbrandHMinusOneProd_card
Documentation

Cardinality of degree-minus-one Tate cohomology for a binary product.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · full declaration
theorem herbrandHMinusOneProd_card
    (σ : G)
    [Finite (HerbrandHMinusOne G A σ)]
    [Finite (HerbrandHMinusOne G B σ)] :
    letI : Finite (HerbrandHMinusOne G (A × B) σ) :=
      herbrandHMinusOneProdFinite A B σ
    Nat.card (HerbrandHMinusOne G (A × B) σ) =
      Nat.card (HerbrandHMinusOne G A σ) *
        Nat.card (HerbrandHMinusOne G B σ) := by
  rw [Nat.card_congr
      (herbrandHMinusOneProdEquiv A B σ).toEquiv,
    Nat.card_prod]
theorem

herbrandQuotient_prod

L209 ↗
CyclicCohomology.herbrandQuotient_prod
Documentation

The Herbrand quotient of a binary product is the product of the two Herbrand quotients.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA
variable {G : Type uG} [Group G] [Fintype G]
variable (A B : Type uA)
variable [CommGroup A] [CommGroup B]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
Lean source · full declaration
theorem herbrandQuotient_prod
    (σ : G)
    [Finite (HerbrandH0 G A)]
    [Finite (HerbrandHMinusOne G A σ)]
    [Finite (HerbrandH0 G B)]
    [Finite (HerbrandHMinusOne G B σ)] :
    letI : Finite (HerbrandH0 G (A × B)) :=
      herbrandH0ProdFinite A B
    letI : Finite (HerbrandHMinusOne G (A × B) σ) :=
      herbrandHMinusOneProdFinite A B σ
    herbrandQuotient (G := G) (A := A × B) σ =
      herbrandQuotient (G := G) (A := A) σ *
        herbrandQuotient (G := G) (A := B) σ := by
  let : Finite (HerbrandH0 G (A × B)) :=
    herbrandH0ProdFinite A B
  let : Finite (HerbrandHMinusOne G (A × B) σ) :=
    herbrandHMinusOneProdFinite A B σ
  rw [herbrandQuotient_eq_card_ratio,
    herbrandQuotient_eq_card_ratio,
    herbrandQuotient_eq_card_ratio,
    herbrandH0Prod_card A B,
    herbrandHMinusOneProd_card A B σ]
  simp only [Nat.cast_mul]
  exact (div_mul_div_comm _ _ _ _).symm

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