Module

Basic.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Basic

109 declarations indexed from sourceView source ↗

Module documentation

Low-degree Herbrand quotients

This reusable implementation supplies the low-degree cyclic cohomology used by the class-formation and local class field theory layers.

Imports9

Mathlib.SetTheory.Cardinal.Finite
Mathlib.Algebra.BigOperators.Group.Finset.Basic
Mathlib.Data.Set.Finite.Range
Mathlib.GroupTheory.Coset.Card
Mathlib.GroupTheory.GroupAction.Basic
Mathlib.GroupTheory.Index
Mathlib.GroupTheory.OrderOfElement
Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.GroupTheory.SpecificGroups.Cyclic

Imported by9

def

smul_eq_of_mem_zpowers_of_sigmaMinusOne_eq_one

L70 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.smul_eq_of_mem_zpowers_of_sigmaMinusOne_eq_one

Documentation

A σ-coboundary equal to 1 makes every element of the cyclic subgroup generated by σ fix the point.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem smul_eq_of_mem_zpowers_of_sigmaMinusOne_eq_one
    {σ g : G} {a : A} (hg : g ∈ Subgroup.zpowers σ)
    (hσ : sigmaMinusOne G A σ a = 1) :
    g • a = a

theorem

fixed_of_forall_mem_zpowers_of_sigmaMinusOne_eq_one

L82 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.fixed_of_forall_mem_zpowers_of_sigmaMinusOne_eq_one

Documentation

If σ generates G, then a trivial σ-coboundary is genuinely fixed by all of G.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem fixed_of_forall_mem_zpowers_of_sigmaMinusOne_eq_one
    {σ : G} {a : A} (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    (hσ : sigmaMinusOne G A σ a = 1) :
    ∀ g : G, g • a = a

theorem

monoidHom_card_eq_card_ker_mul_card_range

L96 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.monoidHom_card_eq_card_ker_mul_card_range

Documentation

First-isomorphism cardinality source for finite exactness calculations: the cardinality of the source of a group homomorphism is the product of the cardinalities of its kernel and range.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem monoidHom_card_eq_card_ker_mul_card_range
    {X : Type uA} {Y : Type uB} [Group X] [Group Y] [Finite X] (f : X →* Y) :
    Nat.card X = Nat.card (MonoidHom.ker f) * Nat.card (MonoidHom.range f)

theorem

monoidHom_card_eq_card_range_mul_card_range_of_exact

L108 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.monoidHom_card_eq_card_range_mul_card_range_of_exact

Documentation

Cardinality source for one exact spot of a group-hom sequence. If range f = ker g, then the middle group has cardinality #range(f) * #range(g).

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem monoidHom_card_eq_card_range_mul_card_range_of_exact
    {X : Type uA} {Y : Type uB} {Z : Type uC} [Group X] [Group Y] [Group Z]
    [Finite Y]
    (f : X →* Y) (g : Y →* Z)
    (hexact : MonoidHom.range f = MonoidHom.ker g) :
    Nat.card Y = Nat.card (MonoidHom.range f) * Nat.card (MonoidHom.range g)

theorem

rightRegularFunctionMulDistribMulAction

L132 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunctionMulDistribMulAction

Documentation

The multiplicative induced module from the trivial subgroup, represented as functions on G with the right-regular action. This is the concrete model used in the low-degree Herbrand comparison.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · full declaration

def rightRegularFunctionMulDistribMulAction :
    MulDistribMulAction G (G → B) where
  smul g f := fun x => f (x * g)
  one_smul := by
    intro f
    change (fun x => f (x * 1)) = f
    funext x
    rw [mul_one]
  mul_smul := by
    intro g h f
    change (fun x => f (x * (g * h))) = fun x => f ((x * g) * h)
    funext x
    rw [mul_assoc]
  smul_mul := by
    intro g f h
    funext x
    rfl
  smul_one := by
    intro g
    funext x
    rfl

theorem

sigmaMinusOneHom_ker_eq_fixedSubgroup

L269 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.sigmaMinusOneHom_ker_eq_fixedSubgroup

Documentation

If σ generates G, the kernel of a ↦ a^(σ-1) is the fixed subgroup.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem sigmaMinusOneHom_ker_eq_fixedSubgroup
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) :
    MonoidHom.ker (sigmaMinusOneHom (G := G) (A := A) σ) = fixedSubgroup G A

theorem

card_eq_card_normKernelSubgroup_mul_card_tateNormSubgroup

L285 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.card_eq_card_normKernelSubgroup_mul_card_tateNormSubgroup

Documentation

Finite-module source: the norm homomorphism factors the cardinality of A into norm-kernel and norm-image cardinalities.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem card_eq_card_normKernelSubgroup_mul_card_tateNormSubgroup [Finite A] :
    Nat.card A = Nat.card (normKernelSubgroup G A) * Nat.card (tateNormSubgroup G A)

theorem

card_eq_card_fixedSubgroup_mul_card_augmentationSubgroup

L295 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.card_eq_card_fixedSubgroup_mul_card_augmentationSubgroup

Documentation

Finite-module source: for a cyclic generator σ, the coboundary homomorphism factors the cardinality of A into fixed and augmentation cardinalities.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem card_eq_card_fixedSubgroup_mul_card_augmentationSubgroup
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) [Finite A] :
    Nat.card A = Nat.card (fixedSubgroup G A) * Nat.card (augmentationSubgroup G A σ)

theorem

herbrand_finite_module_cardinality_balance

L307 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrand_finite_module_cardinality_balance

Documentation

Finite-module cardinality balance behind h(G,A)=1: for a finite cyclic group action, the product #A^G · #I_G A equals #ker N_G · #N_G A.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem herbrand_finite_module_cardinality_balance
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) [Finite A] :
    Nat.card (fixedSubgroup G A) * Nat.card (augmentationSubgroup G A σ) =
      Nat.card (normKernelSubgroup G A) * Nat.card (tateNormSubgroup G A)

def

liftOn

L591 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0.liftOn

Documentation

Evaluate a function on H⁰(G,A) from a representative-level function which is invariant under equality of canonical quotient classes. This is the non-homomorphic elimination API; clients never need the underlying quotient relation.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

def HerbrandH0.liftOn {M : Sort*}
    (q : HerbrandH0 G A) (f : fixedSubgroup G A → M)
    (_h : ∀ a b, HerbrandH0.mk a = HerbrandH0.mk b → f a = f b) : M

theorem

liftOn_mk

L600 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0.liftOn_mk

Documentation

Eliminating a canonical degree-zero class evaluates the representative-level function.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem HerbrandH0.liftOn_mk {M : Sort*}
    (f : fixedSubgroup G A → M)
    (h : ∀ a b, HerbrandH0.mk a = HerbrandH0.mk b → f a = f b)
    (a : fixedSubgroup G A) :
    HerbrandH0.liftOn (HerbrandH0.mk a) f h = f a

def

liftOn

L614 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne.liftOn

Documentation

Evaluate a function on H⁻¹(G,A) from a representative-level function which is invariant under equality of canonical quotient classes.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

def HerbrandHMinusOne.liftOn {M : Sort*} (σ : G)
    (q : HerbrandHMinusOne G A σ) (f : normKernelSubgroup G A → M)
    (_h : ∀ a b,
      HerbrandHMinusOne.mk σ a = HerbrandHMinusOne.mk σ b → f a = f b) : M

theorem

liftOn_mk

L625 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne.liftOn_mk

Documentation

Eliminating a canonical degree-minus-one class evaluates the representative-level function.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem HerbrandHMinusOne.liftOn_mk {M : Sort*} (σ : G)
    (f : normKernelSubgroup G A → M)
    (h : ∀ a b,
      HerbrandHMinusOne.mk σ a = HerbrandHMinusOne.mk σ b → f a = f b)
    (a : normKernelSubgroup G A) :
    HerbrandHMinusOne.liftOn σ (HerbrandHMinusOne.mk σ a) f h = f a

def

lift

L640 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0.lift

Documentation

Descend a homomorphism on fixed points through H⁰(G,A).

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

def HerbrandH0.lift {M : Type*} [Group M]
    (f : fixedSubgroup G A →* M)
    (h : (tateNormSubgroup G A).subgroupOf (fixedSubgroup G A) ≤ f.ker) :
    HerbrandH0 G A →* M

def

lift

L651 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne.lift

Documentation

Descend a homomorphism on the norm kernel through H⁻¹(G,A).

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

def HerbrandHMinusOne.lift {M : Type*} [Group M] (σ : G)
    (f : normKernelSubgroup G A →* M)
    (h : (augmentationSubgroup G A σ).subgroupOf (normKernelSubgroup G A) ≤
      f.ker) : HerbrandHMinusOne G A σ →* M

theorem

lift_mk

L663 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0.lift_mk

Documentation

A homomorphism descended through degree-zero Herbrand cohomology agrees on representatives.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem HerbrandH0.lift_mk {M : Type*} [Group M]
    (f : fixedSubgroup G A →* M)
    (h : (tateNormSubgroup G A).subgroupOf (fixedSubgroup G A) ≤ f.ker)
    (a : fixedSubgroup G A) : HerbrandH0.lift f h (HerbrandH0.mk a) = f a

theorem

lift_mk

L674 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne.lift_mk

Documentation

A homomorphism descended through degree-minus-one Herbrand cohomology agrees on representatives.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem HerbrandHMinusOne.lift_mk {M : Type*} [Group M] (σ : G)
    (f : normKernelSubgroup G A →* M)
    (h : (augmentationSubgroup G A σ).subgroupOf (normKernelSubgroup G A) ≤
      f.ker) (a : normKernelSubgroup G A) :
    HerbrandHMinusOne.lift σ f h (HerbrandHMinusOne.mk σ a) = f a

instance

herbrandH0FiniteOfFinite

L684 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandH0FiniteOfFinite

Documentation

Degree-zero Herbrand cohomology is finite when the coefficient group is finite.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

instance herbrandH0FiniteOfFinite [Finite A] :
    Finite (HerbrandH0 G A)

instance

herbrandHMinusOneFiniteOfFinite

L694 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandHMinusOneFiniteOfFinite

Documentation

Degree-minus-one Herbrand cohomology is finite when the coefficient group is finite.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

instance herbrandHMinusOneFiniteOfFinite (σ : G) [Finite A] :
    Finite (HerbrandHMinusOne G A σ)

abbrev

rightRegularFunctionFixedSubgroup

L705 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunctionFixedSubgroup

Documentation

Fixed subgroup of the right-regular multiplicative induced module.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

abbrev rightRegularFunctionFixedSubgroup : Subgroup (G → B)

abbrev

rightRegularFunctionTateNormSubgroup

L713 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunctionTateNormSubgroup

Documentation

Norm image subgroup of the right-regular multiplicative induced module.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

abbrev rightRegularFunctionTateNormSubgroup : Subgroup (G → B)

def

rightRegularFunctionHerbrandH0

L721 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunctionHerbrandH0

Documentation

H⁰ of the right-regular multiplicative induced module.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

def rightRegularFunctionHerbrandH0

instance

rightRegularFunctionHerbrandH0CommGroup

L729 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunctionHerbrandH0CommGroup

Documentation

Degree-zero Herbrand cohomology of right-regular functions is a commutative group.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

instance rightRegularFunctionHerbrandH0CommGroup :
    CommGroup (rightRegularFunctionHerbrandH0 (G := G) (B := B))

abbrev

rightRegularFunctionNormKernelSubgroup

L739 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunctionNormKernelSubgroup

Documentation

Norm-kernel subgroup of the right-regular multiplicative induced module.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

abbrev rightRegularFunctionNormKernelSubgroup : Subgroup (G → B)

abbrev

rightRegularFunctionAugmentationSubgroup

L747 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunctionAugmentationSubgroup

Documentation

Augmentation subgroup of the right-regular multiplicative induced module.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

abbrev rightRegularFunctionAugmentationSubgroup (σ : G) : Subgroup (G → B)

def

rightRegularFunctionHerbrandHMinusOne

L755 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunctionHerbrandHMinusOne

Documentation

H^{-1} of the right-regular multiplicative induced module.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

def rightRegularFunctionHerbrandHMinusOne (σ : G)

instance

rightRegularFunctionHerbrandHMinusOneCommGroup

L763 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunctionHerbrandHMinusOneCommGroup

Documentation

Degree-minus-one Herbrand cohomology of right-regular functions is a commutative group.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

instance rightRegularFunctionHerbrandHMinusOneCommGroup (σ : G) :
    CommGroup
      (rightRegularFunctionHerbrandHMinusOne (G := G) (B := B) σ)

theorem

tateNorm_sigmaMinusOne_eq_one

L772 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.tateNorm_sigmaMinusOne_eq_one

Documentation

The norm of a multiplicative coboundary is trivial. This is the calculation N_G(b^(σ-1)) = 1 used in the low-degree cyclic-cohomology exact sequence.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
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 tateNorm_sigmaMinusOne_eq_one (σ : G) (a : A) :
    tateNorm G A (sigmaMinusOne G A σ a) = 1

theorem

augmentationSubgroup_le_normKernelSubgroup

L793 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.augmentationSubgroup_le_normKernelSubgroup

Documentation

The augmentation image lies in the norm kernel.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
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 augmentationSubgroup_le_normKernelSubgroup (σ : G) :
    augmentationSubgroup G A σ ≤ normKernelSubgroup G A

theorem

smul_tateNorm_eq

L801 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.smul_tateNorm_eq

Documentation

The norm is fixed by every group element, placing N_G b in A^G in the low-degree cyclic-cohomology exact sequence.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
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 smul_tateNorm_eq (h : G) (a : A) :
    h • tateNorm G A a = tateNorm G A a

theorem

tateNormSubgroup_le_fixedSubgroup

L819 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.tateNormSubgroup_le_fixedSubgroup

Documentation

The norm image lies in the fixed subgroup, as in Herbrand-quotient theory.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
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 tateNormSubgroup_le_fixedSubgroup :
    tateNormSubgroup G A ≤ fixedSubgroup G A

theorem

herbrandH0_subsingleton_of_fixed_le_tateNormSubgroup

L829 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandH0_subsingleton_of_fixed_le_tateNormSubgroup

Documentation

A quotient-level criterion for vanishing of H⁰: if every fixed point is a norm, then the low-degree Herbrand H⁰ quotient is a subsingleton.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem herbrandH0_subsingleton_of_fixed_le_tateNormSubgroup
    (h : fixedSubgroup G A ≤ tateNormSubgroup G A) :
    Subsingleton (HerbrandH0 G A)

theorem

herbrandH0_subsingleton_iff_fixed_le_tateNormSubgroup

L847 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandH0_subsingleton_iff_fixed_le_tateNormSubgroup

Documentation

Degree-zero Herbrand cohomology is trivial exactly when every fixed element is a Tate norm.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
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 herbrandH0_subsingleton_iff_fixed_le_tateNormSubgroup :
    Subsingleton (HerbrandH0 G A) ↔
      fixedSubgroup G A ≤ tateNormSubgroup G A

theorem

herbrandHMinusOne_subsingleton_of_normKernel_le_augmentationSubgroup

L862 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandHMinusOne_subsingleton_of_normKernel_le_augmentationSubgroup

Documentation

A quotient-level criterion for vanishing of H^{-1}: if every norm-kernel element is an augmentation element, then the low-degree Herbrand H^{-1} quotient is a subsingleton.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem herbrandHMinusOne_subsingleton_of_normKernel_le_augmentationSubgroup
    (σ : G) (h : normKernelSubgroup G A ≤ augmentationSubgroup G A σ) :
    Subsingleton (HerbrandHMinusOne G A σ)

theorem

herbrandHMinusOne_subsingleton_iff_normKernel_le_augmentationSubgroup

L882 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandHMinusOne_subsingleton_iff_normKernel_le_augmentationSubgroup

Documentation

Degree-minus-one Herbrand cohomology is trivial exactly when every norm-kernel element is an augmentation element.

Source context 9 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
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 herbrandHMinusOne_subsingleton_iff_normKernel_le_augmentationSubgroup
    (σ : G) :
    Subsingleton (HerbrandHMinusOne G A σ) ↔
      normKernelSubgroup G A ≤ augmentationSubgroup G A σ

theorem

mulEquiv_symm_commutes_smul

L895 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.mulEquiv_symm_commutes_smul

Documentation

The inverse of an equivariant multiplicative equivalence is equivariant.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup C] [MulDistribMulAction G C] in

Lean source · statement

theorem mulEquiv_symm_commutes_smul
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A), e (g • a) = g • e a) :
    ∀ (g : G) (b : B), e.symm (g • b) = g • e.symm b

theorem

fixed_le_tateNormSubgroup_of_mulEquiv

L909 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.fixed_le_tateNormSubgroup_of_mulEquiv

Documentation

Transport the H⁰ vanishing source A^G ≤ N_G A across an equivariant multiplicative equivalence.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup C] [MulDistribMulAction G C] in

Lean source · statement

theorem fixed_le_tateNormSubgroup_of_mulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A), e (g • a) = g • e a)
    (hB : fixedSubgroup G B ≤ tateNormSubgroup G B) :
    fixedSubgroup G A ≤ tateNormSubgroup G A

theorem

normKernel_le_augmentationSubgroup_of_mulEquiv

L932 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.normKernel_le_augmentationSubgroup_of_mulEquiv

Documentation

Transport the H^{-1} vanishing source ker N_G ≤ I_G A across an equivariant multiplicative equivalence.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup C] [MulDistribMulAction G C] in

Lean source · statement

theorem normKernel_le_augmentationSubgroup_of_mulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A), e (g • a) = g • e a)
    (σ : G) (hB : normKernelSubgroup G B ≤ augmentationSubgroup G B σ) :
    normKernelSubgroup G A ≤ augmentationSubgroup G A σ

theorem

herbrandH0_subsingleton_of_mulEquiv

L962 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandH0_subsingleton_of_mulEquiv

Documentation

Transport low-degree H⁰ triviality across an equivariant multiplicative equivalence.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup C] [MulDistribMulAction G C] in

Lean source · statement

theorem herbrandH0_subsingleton_of_mulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A), e (g • a) = g • e a)
    (hB : fixedSubgroup G B ≤ tateNormSubgroup G B) :
    Subsingleton (HerbrandH0 G A)

theorem

herbrandHMinusOne_subsingleton_of_mulEquiv

L974 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandHMinusOne_subsingleton_of_mulEquiv

Documentation

Transport low-degree H^{-1} triviality across an equivariant multiplicative equivalence.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup C] [MulDistribMulAction G C] in

Lean source · statement

theorem herbrandHMinusOne_subsingleton_of_mulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A), e (g • a) = g • e a)
    (σ : G) (hB : normKernelSubgroup G B ≤ augmentationSubgroup G B σ) :
    Subsingleton (HerbrandHMinusOne G A σ)

theorem

rightRegularFunction_mem_normKernelSubgroup_iff

L989 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunction_mem_normKernelSubgroup_iff

Documentation

Membership in the right-regular norm kernel is the single product condition ∏ g, f g = 1.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularFunction_mem_normKernelSubgroup_iff (f : G → B) :
    f ∈ rightRegularFunctionNormKernelSubgroup (G := G) (B := B) ↔
      (∏ g : G, f g) = 1

def

rightRegularCyclicPartialProduct

L1035 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicPartialProduct

Documentation

The partial primitive along the cyclic powers of σ. This is the candidate used to solve b (x * σ) * (b x)⁻¹ = f x on the right-regular induced module.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

def rightRegularCyclicPartialProduct (σ : G) (f : G → B) (i : ℕ) : B

theorem

rightRegularCyclicPartialProduct_zero

L1042 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicPartialProduct_zero

Documentation

The partial primitive starts at 1.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicPartialProduct_zero (σ : G) (f : G → B) :
    rightRegularCyclicPartialProduct (G := G) (B := B) σ f 0 = 1

theorem

rightRegularCyclicPartialProduct_succ

L1050 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicPartialProduct_succ

Documentation

Successor step for the cyclic partial primitive.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicPartialProduct_succ (σ : G) (f : G → B) (i : ℕ) :
    rightRegularCyclicPartialProduct (G := G) (B := B) σ f (i + 1) =
      rightRegularCyclicPartialProduct (G := G) (B := B) σ f i * f (σ ^ i)

theorem

rightRegularCyclicPartialProduct_succ_mul_inv

L1060 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicPartialProduct_succ_mul_inv

Documentation

The successor step is the desired coboundary equation away from the wrap-around point.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicPartialProduct_succ_mul_inv
    (σ : G) (f : G → B) (i : ℕ) :
    rightRegularCyclicPartialProduct (G := G) (B := B) σ f (i + 1) *
        (rightRegularCyclicPartialProduct (G := G) (B := B) σ f i)⁻¹ =
      f (σ ^ i)

theorem

rightRegularCyclicPartialProduct_wrap_mul_inv_of_eq_one

L1073 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicPartialProduct_wrap_mul_inv_of_eq_one

Documentation

The product-one condition gives the wrap-around coboundary equation for the cyclic partial primitive.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicPartialProduct_wrap_mul_inv_of_eq_one
    (σ : G) (f : G → B) {n : ℕ} (hn : 0 < n)
    (hprod : rightRegularCyclicPartialProduct (G := G) (B := B) σ f n = 1) :
    rightRegularCyclicPartialProduct (G := G) (B := B) σ f 0 *
        (rightRegularCyclicPartialProduct (G := G) (B := B) σ f (n - 1))⁻¹ =
      f (σ ^ (n - 1))

def

rightRegularCyclicIndex

L1095 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicIndex

Documentation

The canonical ZMod |G| index of a group element with respect to a chosen cyclic generator.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

def rightRegularCyclicIndex
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) (x : G) :
    ZMod (Fintype.card G)

theorem

rightRegularCyclicIndex_spec

L1104 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicIndex_spec

Documentation

The cyclic index represents the original group element.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicIndex_spec
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) (x : G) :
    x = σ ^ (rightRegularCyclicIndex (G := G) σ hgen x).val

theorem

rightRegularCyclicIndex_eq_of_repr

L1115 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicIndex_eq_of_repr

Documentation

If a concrete ZMod |G| representative is known, the cyclic index chooser returns it.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicIndex_eq_of_repr
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    {x : G} {m : ZMod (Fintype.card G)} (hm : x = σ ^ m.val) :
    rightRegularCyclicIndex (G := G) σ hgen x = m

theorem

rightRegularCyclicIndex_val_pow_of_lt

L1126 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicIndex_val_pow_of_lt

Documentation

On natural powers in the standard range, the cyclic index has the expected value.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicIndex_val_pow_of_lt
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    {i : ℕ} (hi : i < Fintype.card G) :
    (rightRegularCyclicIndex (G := G) σ hgen (σ ^ i)).val = i

def

rightRegularCyclicPrimitive

L1142 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicPrimitive

Documentation

The group-element-indexed primitive candidate obtained from the cyclic partial products.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

def rightRegularCyclicPrimitive
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) (f : G → B) : G → B

theorem

rightRegularCyclicPrimitive_mul_sigma_mul_inv_of_index_succ_lt

L1153 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicPrimitive_mul_sigma_mul_inv_of_index_succ_lt

Documentation

Away from the wrap-around index, the cyclic primitive solves the right-regular coboundary equation.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicPrimitive_mul_sigma_mul_inv_of_index_succ_lt
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) (f : G → B) (x : G)
    (hix : (rightRegularCyclicIndex (G := G) σ hgen x).val + 1 < Fintype.card G) :
    rightRegularCyclicPrimitive (G := G) (B := B) σ hgen f (x * σ) *
        (rightRegularCyclicPrimitive (G := G) (B := B) σ hgen f x)⁻¹ =
      f x

theorem

rightRegularCyclicPrimitive_mul_sigma_mul_inv_of_index_eq_card_sub_one

L1184 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicPrimitive_mul_sigma_mul_inv_of_index_eq_card_sub_one

Documentation

At the wrap-around index, the product-one condition makes the cyclic primitive solve the right-regular coboundary equation.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicPrimitive_mul_sigma_mul_inv_of_index_eq_card_sub_one
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) (f : G → B) (x : G)
    (hix : (rightRegularCyclicIndex (G := G) σ hgen x).val = Fintype.card G - 1)
    (hprod :
      rightRegularCyclicPartialProduct (G := G) (B := B) σ f (Fintype.card G) = 1) :
    rightRegularCyclicPrimitive (G := G) (B := B) σ hgen f (x * σ) *
        (rightRegularCyclicPrimitive (G := G) (B := B) σ hgen f x)⁻¹ =
      f x

theorem

rightRegularCyclicPrimitive_mul_sigma_mul_inv_of_partialProduct_eq_one

L1239 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularCyclicPrimitive_mul_sigma_mul_inv_of_partialProduct_eq_one

Documentation

If the cyclic partial product over a full period is 1, the group-indexed cyclic primitive solves the right-regular coboundary equation at every point.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularCyclicPrimitive_mul_sigma_mul_inv_of_partialProduct_eq_one
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) (f : G → B)
    (hprod :
      rightRegularCyclicPartialProduct (G := G) (B := B) σ f (Fintype.card G) = 1)
    (x : G) :
    rightRegularCyclicPrimitive (G := G) (B := B) σ hgen f (x * σ) *
        (rightRegularCyclicPrimitive (G := G) (B := B) σ hgen f x)⁻¹ =
      f x

theorem

rightRegularFunction_prod_powers_eq_one_of_mem_normKernel

L1269 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunction_prod_powers_eq_one_of_mem_normKernel

Documentation

A right-regular norm-kernel element has product 1 along one full cyclic enumeration by a generator.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · full declaration

theorem rightRegularFunction_prod_powers_eq_one_of_mem_normKernel
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    {f : G → B}
    (hf : f ∈ rightRegularFunctionNormKernelSubgroup (G := G) (B := B)) :
    (Finset.range (Nat.card G)).prod (fun i => f (σ ^ i)) = 1 := by
  classical
  have hprod : (∏ g : G, f g) = 1 :=
    (rightRegularFunction_mem_normKernelSubgroup_iff (G := G) (B := B) f).1 hf
  have hcard : orderOf σ = Nat.card G :=
    orderOf_eq_card_of_forall_mem_zpowers (g := σ) hgen
  have hinj : Set.InjOn (fun i : ℕ => σ ^ i) (Finset.range (Nat.card G) : Set ℕ) := by
    intro i hi j hj hij
    have hmod : i ≡ j [MOD orderOf σ] := (pow_eq_pow_iff_modEq (x := σ)).1 hij
    rw [hcard] at hmod
    exact Nat.ModEq.eq_of_lt_of_lt hmod (by simpa using hi) (by simpa using hj)
  have himage :
      Finset.image (fun i : ℕ => σ ^ i) (Finset.range (Nat.card G)) = Finset.univ :=
    IsCyclic.image_range_card (a := σ) hgen
  calc
    (Finset.range (Nat.card G)).prod (fun i => f (σ ^ i)) =
        (Finset.image (fun i : ℕ => σ ^ i) (Finset.range (Nat.card G))).prod
          (fun x => f x) := by
      exact (Finset.prod_image (s := Finset.range (Nat.card G))
        (g := fun i : ℕ => σ ^ i) (f := f) hinj).symm
    _ = ∏ x : G, f x := by
      rw [himage]
    _ = 1 := hprod

theorem

rightRegularFunction_mem_augmentationSubgroup_iff

L1302 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunction_mem_augmentationSubgroup_iff

Documentation

Membership in the right-regular augmentation subgroup is the pointwise difference equation b (x * σ) * (b x)⁻¹ = f x.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularFunction_mem_augmentationSubgroup_iff
    (σ : G) (f : G → B) :
    f ∈ rightRegularFunctionAugmentationSubgroup (G := G) (B := B) σ ↔
      ∃ b : G → B, ∀ x : G, b (x * σ) * (b x)⁻¹ = f x

theorem

rightRegularFunction_normKernel_le_augmentationSubgroup

L1328 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunction_normKernel_le_augmentationSubgroup

Documentation

Concrete H^{-1} source for the right-regular multiplicative induced module: every norm-kernel element is an augmentation element.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularFunction_normKernel_le_augmentationSubgroup
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) :
    rightRegularFunctionNormKernelSubgroup (G := G) (B := B) ≤
      rightRegularFunctionAugmentationSubgroup (G := G) (B := B) σ

theorem

rightRegularFunction_herbrandHMinusOne_subsingleton

L1351 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunction_herbrandHMinusOne_subsingleton

Documentation

The H^{-1} quotient of the right-regular multiplicative induced module is trivial for a cyclic group generated by σ.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularFunction_herbrandHMinusOne_subsingleton
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) :
    Subsingleton (rightRegularFunctionHerbrandHMinusOne (G := G) (B := B) σ)

theorem

rightRegularFunction_fixed_le_tateNormSubgroup

L1365 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunction_fixed_le_tateNormSubgroup

Documentation

Concrete H⁰ source for induced modules: for the right-regular multiplicative induced module G → B, every fixed point is a norm.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularFunction_fixed_le_tateNormSubgroup :
    rightRegularFunctionFixedSubgroup (G := G) (B := B) ≤
      rightRegularFunctionTateNormSubgroup (G := G) (B := B)

theorem

rightRegularFunction_herbrandH0_subsingleton

L1423 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.rightRegularFunction_herbrandH0_subsingleton

Documentation

The H⁰ quotient of the right-regular multiplicative induced module is trivial. This is the degree-zero half of the low-degree Herbrand comparison.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · statement

theorem rightRegularFunction_herbrandH0_subsingleton :
    Subsingleton (rightRegularFunctionHerbrandH0 (G := G) (B := B))

theorem

herbrandH0_subsingleton_of_equiv_rightRegularFunction

L1433 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandH0_subsingleton_of_equiv_rightRegularFunction

Documentation

Transport H⁰ vanishing from the right-regular trivial-subgroup model along an explicit multiplicative equivalence.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup C] [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem herbrandH0_subsingleton_of_equiv_rightRegularFunction
    (e : A ≃* (G → B))
    (he : ∀ (g : G) (a : A) (x : G), e (g • a) x = e a (x * g)) :
    Subsingleton (HerbrandH0 G A)

theorem

herbrandHMinusOne_subsingleton_of_equiv_rightRegularFunction

L1450 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandHMinusOne_subsingleton_of_equiv_rightRegularFunction

Documentation

Transport H^{-1} vanishing from the right-regular trivial-subgroup model along an explicit multiplicative equivalence.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup C] [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem herbrandHMinusOne_subsingleton_of_equiv_rightRegularFunction
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    (e : A ≃* (G → B))
    (he : ∀ (g : G) (a : A) (x : G), e (g • a) x = e a (x * g)) :
    Subsingleton (HerbrandHMinusOne G A σ)

def

multiplicativeMulDistribMulActionOfDistribMulAction

L1472 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.multiplicativeMulDistribMulActionOfDistribMulAction

Documentation

A distributive action on an additive group induces a multiplicative action on its Multiplicative wrapper.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · full declaration

def multiplicativeMulDistribMulActionOfDistribMulAction
    (G : Type uG) (M : Type uA) [Group G] [AddCommGroup M]
    [DistribMulAction G M] :
    MulDistribMulAction G (Multiplicative M) where
  smul g m := Multiplicative.ofAdd (g • Multiplicative.toAdd m)
  one_smul := by
    intro m
    change Multiplicative.ofAdd (1 • Multiplicative.toAdd m) =
      Multiplicative.ofAdd (Multiplicative.toAdd m)
    rw [one_smul]
  mul_smul := by
    intro g h m
    change Multiplicative.ofAdd ((g * h) • Multiplicative.toAdd m) =
      Multiplicative.ofAdd (g • h • Multiplicative.toAdd m)
    rw [mul_smul]
  smul_mul := by
    intro g m n
    change Multiplicative.ofAdd (g • Multiplicative.toAdd (m * n)) =
      Multiplicative.ofAdd
        (g • Multiplicative.toAdd m + g • Multiplicative.toAdd n)
    rw [show Multiplicative.toAdd (m * n) =
        Multiplicative.toAdd m + Multiplicative.toAdd n from rfl]
    rw [smul_add]
  smul_one := by
    intro g
    change Multiplicative.ofAdd (g • (0 : M)) = Multiplicative.ofAdd (0 : M)
    rw [smul_zero]

def

multiplicativeFunctionMulEquiv

L1505 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.multiplicativeFunctionMulEquiv

Documentation

Pointwise conversion between a multiplicative wrapper on additive functions and functions into the multiplicative wrapper.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · full declaration

def multiplicativeFunctionMulEquiv
    (G : Type uG) (D : Type uB) [AddCommGroup D] :
    Multiplicative (G → D) ≃* (G → Multiplicative D) where
  toFun f := fun x => Multiplicative.ofAdd (Multiplicative.toAdd f x)
  invFun f := Multiplicative.ofAdd (fun x => Multiplicative.toAdd (f x))
  left_inv := by
    intro f
    rfl
  right_inv := by
    intro f
    funext x
    rfl
  map_mul' := by
    intro f h
    funext x
    rfl

def

mulEquivRightRegularFunctionOfAddEquiv

L1527 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.mulEquivRightRegularFunctionOfAddEquiv

Documentation

Convert an additive equivalence with a function space into the multiplicative right-regular function model used by the Herbrand quotient API.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · full declaration

def mulEquivRightRegularFunctionOfAddEquiv
    (G : Type uG) {M : Type uA} {D : Type uB}
    [AddCommGroup M] [AddCommGroup D] (e : M ≃+ (G → D)) :
    Multiplicative M ≃* (G → Multiplicative D) where
  toFun m := fun x => Multiplicative.ofAdd (e (Multiplicative.toAdd m) x)
  invFun f := Multiplicative.ofAdd (e.symm (fun x => Multiplicative.toAdd (f x)))
  left_inv := by
    intro m
    change Multiplicative.ofAdd
        (e.symm (e (Multiplicative.toAdd m))) =
      Multiplicative.ofAdd (Multiplicative.toAdd m)
    exact congrArg Multiplicative.ofAdd (e.left_inv (Multiplicative.toAdd m))
  right_inv := by
    intro f
    funext x
    change Multiplicative.ofAdd
        (e (e.symm (fun y : G => Multiplicative.toAdd (f y))) x) =
      Multiplicative.ofAdd (Multiplicative.toAdd (f x))
    exact congrArg Multiplicative.ofAdd
      (congrArg (fun q : G → D => q x)
        (e.right_inv (fun y : G => Multiplicative.toAdd (f y))))
  map_mul' := by
    intro m n
    funext x
    change Multiplicative.ofAdd (e (Multiplicative.toAdd (m * n)) x) =
      Multiplicative.ofAdd
        (e (Multiplicative.toAdd m) x + e (Multiplicative.toAdd n) x)
    rw [show Multiplicative.toAdd (m * n) =
        Multiplicative.toAdd m + Multiplicative.toAdd n from rfl]
    exact congrArg Multiplicative.ofAdd
      (congrArg (fun q : G → D => q x)
        (e.map_add (Multiplicative.toAdd m) (Multiplicative.toAdd n)))

theorem

mulEquivRightRegularFunctionOfAddEquiv_commutes

L1565 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.mulEquivRightRegularFunctionOfAddEquiv_commutes

Documentation

Equivariance of mulEquivRightRegularFunctionOfAddEquiv, assuming the input additive equivalence is right-regular equivariant pointwise.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · full declaration

theorem mulEquivRightRegularFunctionOfAddEquiv_commutes
    {M : Type uA} {D : Type uB}
    [AddCommGroup M] [DistribMulAction G M] [AddCommGroup D]
    (e : M ≃+ (G → D))
    (he : ∀ (g : G) (m : M) (x : G), e (g • m) x = e m (x * g))
    (g : G) (m : Multiplicative M) (x : G) :
    letI := multiplicativeMulDistribMulActionOfDistribMulAction G M
    mulEquivRightRegularFunctionOfAddEquiv G e (g • m) x =
      mulEquivRightRegularFunctionOfAddEquiv G e m (x * g) := by
  change Multiplicative.ofAdd (e (g • Multiplicative.toAdd m) x) =
    Multiplicative.ofAdd (e (Multiplicative.toAdd m) (x * g))
  exact congrArg Multiplicative.ofAdd (he g (Multiplicative.toAdd m) x)

theorem

herbrandH0_subsingleton_of_addEquiv_rightRegularFunction

L1583 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandH0_subsingleton_of_addEquiv_rightRegularFunction

Documentation

H⁰ vanishing for a multiplicative wrapper transported from an additive right-regular equivalence.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · full declaration

theorem herbrandH0_subsingleton_of_addEquiv_rightRegularFunction
    {M : Type uA} {D : Type uB}
    [AddCommGroup M] [DistribMulAction G M] [AddCommGroup D]
    (e : M ≃+ (G → D))
    (he : ∀ (g : G) (m : M) (x : G), e (g • m) x = e m (x * g)) :
    letI := multiplicativeMulDistribMulActionOfDistribMulAction G M
    Subsingleton (HerbrandH0 G (Multiplicative M)) := by
  let := multiplicativeMulDistribMulActionOfDistribMulAction G M
  let : MulDistribMulAction G (Multiplicative D) := {
    smul _ d := d
    one_smul := by
      intro d
      rfl
    mul_smul := by
      intro _ _ d
      rfl
    smul_mul := by
      intro _ d e
      rfl
    smul_one := by
      intro _
      rfl
  }
  exact herbrandH0_subsingleton_of_equiv_rightRegularFunction
    (G := G) (A := Multiplicative M) (B := Multiplicative D)
    (mulEquivRightRegularFunctionOfAddEquiv G e)
    (by
      intro g m x
      exact mulEquivRightRegularFunctionOfAddEquiv_commutes
        (G := G) e he g m x)

theorem

herbrandHMinusOne_subsingleton_of_addEquiv_rightRegularFunction

L1619 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandHMinusOne_subsingleton_of_addEquiv_rightRegularFunction

Documentation

H^{-1} vanishing for a multiplicative wrapper transported from an additive right-regular equivalence.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C] in

Lean source · full declaration

theorem herbrandHMinusOne_subsingleton_of_addEquiv_rightRegularFunction
    {M : Type uA} {D : Type uB}
    [AddCommGroup M] [DistribMulAction G M] [AddCommGroup D]
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    (e : M ≃+ (G → D))
    (he : ∀ (g : G) (m : M) (x : G), e (g • m) x = e m (x * g)) :
    letI := multiplicativeMulDistribMulActionOfDistribMulAction G M
    Subsingleton (HerbrandHMinusOne G (Multiplicative M) σ) := by
  let := multiplicativeMulDistribMulActionOfDistribMulAction G M
  let : MulDistribMulAction G (Multiplicative D) := {
    smul _ d := d
    one_smul := by
      intro d
      rfl
    mul_smul := by
      intro _ _ d
      rfl
    smul_mul := by
      intro _ d e
      rfl
    smul_one := by
      intro _
      rfl
  }
  exact herbrandHMinusOne_subsingleton_of_equiv_rightRegularFunction
    (G := G) (A := Multiplicative M) (B := Multiplicative D)
    σ hgen (mulEquivRightRegularFunctionOfAddEquiv G e)
    (by
      intro g m x
      exact mulEquivRightRegularFunctionOfAddEquiv_commutes
        (G := G) e he g m x)

theorem

card_fixedSubgroup_eq_card_herbrandH0_mul_card_tateNormSubgroup

L1654 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.card_fixedSubgroup_eq_card_herbrandH0_mul_card_tateNormSubgroup

Documentation

Quotient-cardinality source for H⁰(G,A)=A^G/N_G A.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem card_fixedSubgroup_eq_card_herbrandH0_mul_card_tateNormSubgroup [Finite A] :
    Nat.card (fixedSubgroup G A) =
      Nat.card (HerbrandH0 G A) * Nat.card (tateNormSubgroup G A)

theorem

card_normKernelSubgroup_eq_card_herbrandHMinusOne_mul_card_augmentationSubgroup

L1666 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.card_normKernelSubgroup_eq_card_herbrandHMinusOne_mul_card_augmentationSubgroup

Documentation

Quotient-cardinality source for H^{-1}(G,A)=ker(N_G)/I_G A.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem card_normKernelSubgroup_eq_card_herbrandHMinusOne_mul_card_augmentationSubgroup
    (σ : G) [Finite A] :
    Nat.card (normKernelSubgroup G A) =
      Nat.card (HerbrandHMinusOne G A σ) *
        Nat.card (augmentationSubgroup G A σ)

theorem

herbrand_finite_module_card_eq

L1680 ↗

CyclicCohomology.ProfiniteCohomology.Herbrand.herbrand_finite_module_card_eq

Documentation

The two low-degree Herbrand quotients of a finite cyclic module have equal cardinality, the finite-module source for Herbrand-quotient multiplicativity.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
open scoped BigOperators
namespace ProfiniteCohomology
namespace Herbrand
universe uG uA uB uC
variable {G : Type uG} {A : Type uA} {B : Type uB} {C : Type uC}
variable [Group G] [Fintype G] [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B] [MulDistribMulAction G C]
omit [CommGroup B] [CommGroup C]
    [MulDistribMulAction G B] [MulDistribMulAction G C] in

Lean source · statement

theorem herbrand_finite_module_card_eq
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ) [Finite A] :
    Nat.card (HerbrandH0 G A) = Nat.card (HerbrandHMinusOne G A σ)

Module documentation

Low-degree Herbrand quotients

Declarations