NYLL
Module

Product.lean

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

Module documentation

Low-degree Tate cohomology of products

This file proves that multiplicative Tate H⁰ and H⁻¹ commute with dependent products, giving the product step for low-degree Herbrand quotients.

Imports1
Imported by8

Declarations

def

piMulDistribMulAction

L28 ↗
CyclicCohomology.piMulDistribMulAction
Documentation

The componentwise multiplicative action on a dependent product.

Source context 4 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
Lean source · full declaration
def piMulDistribMulAction
    (G : Type uG) [Group G]
    {ι : Type uι} (A : ι → Type uA)
    [∀ i, CommGroup (A i)]
    [∀ i, MulDistribMulAction G (A i)] :
    MulDistribMulAction G (∀ i, A i) where
  smul g x i := g • x i
  one_smul x := by
    funext i
    exact one_smul G (x i)
  mul_smul g h x := by
    funext i
    exact mul_smul g h (x i)
  smul_one g := by
    funext i
    exact MulDistribMulAction.smul_one g
  smul_mul g x y := by
    funext i
    exact MulDistribMulAction.smul_mul g (x i) (y i)
def

piSubgroup

L49 ↗
CyclicCohomology.piSubgroup
Documentation

The pointwise product of a family of subgroups.

Source context 4 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
Lean source · full declaration
def piSubgroup (ι : Type uι) (A : ι → Type uA)
    [∀ i, CommGroup (A i)]
    (N : ∀ i, Subgroup (A i)) :
    Subgroup (∀ i, A i) where
  carrier := {x | ∀ i, x i ∈ N i}
  one_mem' i := (N i).one_mem
  mul_mem' hx hy i := (N i).mul_mem (hx i) (hy i)
  inv_mem' hx i := (N i).inv_mem (hx i)
theorem

mem_piSubgroup_iff

L59 ↗
CyclicCohomology.mem_piSubgroup_iff
Source context 4 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
Lean source · statement
theorem mem_piSubgroup_iff
    (ι : Type uι) (A : ι → Type uA)
    [∀ i, CommGroup (A i)]
    (N : ∀ i, Subgroup (A i))
    (x : ∀ i, A i) :
    x ∈ piSubgroup ι A N ↔
      ∀ i, x i ∈ N i
def

piQuotientMap

L69 ↗
CyclicCohomology.piQuotientMap
Documentation

The componentwise quotient map.

Source context 4 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
Lean source · full declaration
def piQuotientMap
    (ι : Type uι) (A : ι → Type uA)
    [∀ i, CommGroup (A i)]
    (N : ∀ i, Subgroup (A i)) :
    (∀ i, A i) →* ∀ i, A i ⧸ N i where
  toFun x i := QuotientGroup.mk' (N i) (x i)
  map_one' := by
    ext i
    exact (QuotientGroup.mk' (N i)).map_one
  map_mul' x y := by
    ext i
    exact (QuotientGroup.mk' (N i)).map_mul
      (x i) (y i)
theorem

piQuotientMap_apply

L84 ↗
CyclicCohomology.piQuotientMap_apply
Source context 4 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
Lean source · statement
theorem piQuotientMap_apply
    (ι : Type uι) (A : ι → Type uA)
    [∀ i, CommGroup (A i)]
    (N : ∀ i, Subgroup (A i))
    (x : ∀ i, A i) (i : ι) :
    piQuotientMap ι A N x i =
      QuotientGroup.mk' (N i) (x i)
theorem

ker_piQuotientMap

L93 ↗
CyclicCohomology.ker_piQuotientMap
Source context 4 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
Lean source · statement
theorem ker_piQuotientMap
    (ι : Type uι) (A : ι → Type uA)
    [∀ i, CommGroup (A i)]
    (N : ∀ i, Subgroup (A i)) :
    (piQuotientMap ι A N).ker =
      piSubgroup ι A N
theorem

piQuotientMap_surjective

L117 ↗
CyclicCohomology.piQuotientMap_surjective
Source context 4 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
Lean source · statement
theorem piQuotientMap_surjective
    (ι : Type uι) (A : ι → Type uA)
    [∀ i, CommGroup (A i)]
    (N : ∀ i, Subgroup (A i)) :
    Function.Surjective (piQuotientMap ι A N)
def

piQuotientEquiv

L131 ↗
CyclicCohomology.piQuotientEquiv
Documentation

The quotient of a dependent product by the pointwise subgroup is the dependent product of the quotients.

Source context 4 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
Lean source · statement
def piQuotientEquiv
    (ι : Type uι) (A : ι → Type uA)
    [∀ i, CommGroup (A i)]
    (N : ∀ i, Subgroup (A i)) :
    (∀ i, A i) ⧸ piSubgroup ι A N ≃*
      ∀ i, A i ⧸ N i
instance

(anonymous instance)

L150 ↗
Source context 9 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
section TateProducts
variable {G : Type uG} [Group G] [Fintype G]
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ i, CommGroup (A i)]
variable [∀ i, MulDistribMulAction G (A i)]
Lean source · statement
instance :
    MulDistribMulAction G (∀ i, A i)
def

fixedPiEquiv

L155 ↗
CyclicCohomology.fixedPiEquiv
Documentation

Fixed points of a product are products of fixed points.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
section TateProducts
variable {G : Type uG} [Group G] [Fintype G]
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ i, CommGroup (A i)]
variable [∀ i, MulDistribMulAction G (A i)]
local instance :
    MulDistribMulAction G (∀ i, A i) :=
  piMulDistribMulAction G A
Lean source · full declaration
def fixedPiEquiv :
    fixedSubgroup G (∀ i, A i) ≃*
      ∀ i, fixedSubgroup G (A i) where
  toFun x i := ⟨x.1 i, fun g ↦ congrFun (x.2 g) i⟩
  invFun x := ⟨fun i ↦ (x i).1, fun g ↦ by
    funext i
    exact (x i).2 g⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
theorem

fixedPiEquiv_apply_coe

L168 ↗
CyclicCohomology.fixedPiEquiv_apply_coe
Source context 11 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
section TateProducts
variable {G : Type uG} [Group G] [Fintype G]
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ i, CommGroup (A i)]
variable [∀ i, MulDistribMulAction G (A i)]
local instance :
    MulDistribMulAction G (∀ i, A i) :=
  piMulDistribMulAction G A
omit [Fintype G] in
Lean source · statement
theorem fixedPiEquiv_apply_coe
    (x : fixedSubgroup G (∀ i, A i))
    (i : ι) :
    ((fixedPiEquiv (G := G) A x i : A i)) =
      x.1 i
def

normKernelPiEquiv

L176 ↗
CyclicCohomology.normKernelPiEquiv
Documentation

Norm kernels of a product are products of norm kernels.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
section TateProducts
variable {G : Type uG} [Group G] [Fintype G]
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ i, CommGroup (A i)]
variable [∀ i, MulDistribMulAction G (A i)]
local instance :
    MulDistribMulAction G (∀ i, A i) :=
  piMulDistribMulAction G A
Lean source · full declaration
def normKernelPiEquiv :
    normKernelSubgroup G (∀ i, A i) ≃*
      ∀ i, normKernelSubgroup G (A i) where
  toFun x i := ⟨x.1 i, by
    change tateNorm G (A i) (x.1 i) = 1
    have hi := congrFun x.2 i
    simpa only [tateNormHom_apply, tateNorm, Finset.prod_apply,
      Pi.smul_apply, Pi.one_apply] using hi⟩
  invFun x := ⟨fun i ↦ (x i).1, by
    funext i
    change
      (tateNorm G (∀ i, A i)
        (fun i ↦ (x i).1)) i = 1
    have hi := (x i).2
    change tateNormHom (G := G) (A := A i) (x i).1 = 1 at hi
    rw [tateNormHom_apply] at hi
    simpa only [tateNorm, Finset.prod_apply,
      Pi.smul_apply] using hi⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
theorem

normKernelPiEquiv_apply_coe

L199 ↗
CyclicCohomology.normKernelPiEquiv_apply_coe
Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
section TateProducts
variable {G : Type uG} [Group G] [Fintype G]
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ i, CommGroup (A i)]
variable [∀ i, MulDistribMulAction G (A i)]
local instance :
    MulDistribMulAction G (∀ i, A i) :=
  piMulDistribMulAction G A
Lean source · statement
theorem normKernelPiEquiv_apply_coe
    (x : normKernelSubgroup G (∀ i, A i))
    (i : ι) :
    ((normKernelPiEquiv (G := G) A x i : A i)) =
      x.1 i
def

herbrandH0PiEquiv

L207 ↗
CyclicCohomology.herbrandH0PiEquiv
Documentation

Tate H⁰ commutes with dependent products.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
section TateProducts
variable {G : Type uG} [Group G] [Fintype G]
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ i, CommGroup (A i)]
variable [∀ i, MulDistribMulAction G (A i)]
local instance :
    MulDistribMulAction G (∀ i, A i) :=
  piMulDistribMulAction G A
Lean source · statement
def herbrandH0PiEquiv :
    HerbrandH0 G (∀ i, A i) ≃*
      ∀ i, HerbrandH0 G (A i)
def

herbrandHMinusOnePiEquiv

L269 ↗
CyclicCohomology.herbrandHMinusOnePiEquiv
Documentation

Tate H⁻¹ commutes with dependent products.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uι uA
section TateProducts
variable {G : Type uG} [Group G] [Fintype G]
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ i, CommGroup (A i)]
variable [∀ i, MulDistribMulAction G (A i)]
local instance :
    MulDistribMulAction G (∀ i, A i) :=
  piMulDistribMulAction G A
Lean source · statement
def herbrandHMinusOnePiEquiv (σ : G) :
    HerbrandHMinusOne G (∀ i, A i) σ ≃*
      ∀ i, HerbrandHMinusOne G (A i) σ

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