NYLL
Module

Induced.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.Induced
50 declarations indexed from sourceView source ↗

Module documentation

Multiplicative induced modules

This file supplies the multiplicative induced-module model used in the Herbrand quotient calculation. If H ≤ G acts on a commutative group B, then Ind_H^G B is represented by the equivariant functions

f : G → B, f (h * x) = h • f x.

The ambient group acts by right translation. This convention is the one used for the products of the local multiplicative groups above a place. The basic equivariant-function model is supplied by ProCGroups.InducedFunctions; this module adds the cyclic-coordinate and Herbrand calculations.

Imports3
Imported by5

Declarations

def

twistedFinRotate

L38 ↗
CyclicCohomology.twistedFinRotate
Documentation

A one-step cyclic rotation whose wrap-around coordinate is acted on by τ.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · statement
def twistedFinRotate {K C : Type*} [Group K] [CommGroup C]
    [MulDistribMulAction K C] {n : ℕ} [NeZero n]
    (τ : K) (v : Fin n → C) (i : Fin n) : C
theorem

prod_twistedFinRotate_div

L45 ↗
CyclicCohomology.prod_twistedFinRotate_div
Documentation

Cancellation of all non-wrap-around factors in a twisted rotation.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · statement
theorem prod_twistedFinRotate_div
    {K C : Type*} [Group K] [CommGroup C]
    [MulDistribMulAction K C] {n : ℕ} [NeZero n]
    (τ : K) (v : Fin n → C) :
    (∏ i : Fin n, twistedFinRotate τ v i) *
        (∏ i : Fin n, v i)⁻¹ =
      τ • v 0 * (v 0)⁻¹
theorem

pow_mul_eq_pow_finRotate

L88 ↗
CyclicCohomology.pow_mul_eq_pow_finRotate
Documentation

Multiplication by the cyclic generator advances finRotate, with the last coordinate wrapping to the full-period power.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · full declaration
theorem pow_mul_eq_pow_finRotate
    {X : Type*} [Monoid X] {n : ℕ} [NeZero n]
    (a : X) (i : Fin n) :
    a ^ i.1 * a =
      if finRotate n i = 0 then a ^ n
      else a ^ (finRotate n i).1 := by
  cases n with
  | zero => exact Fin.elim0 i
  | succ n =>
      by_cases hi : i = Fin.last n
      · subst i
        simp [pow_succ]
      · have hil : i.1 < n :=
          Fin.val_lt_last hi
        rw [finRotate_of_lt hil]
        simp [pow_succ]
def

finPartialProduct

L106 ↗
CyclicCohomology.finPartialProduct
Documentation

Partial product of a finite vector.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · statement
def finPartialProduct {C : Type*} [CommMonoid C]
    {n : ℕ} (v : Fin n → C) (k : ℕ) : C
theorem

finPartialProduct_zero

L112 ↗
CyclicCohomology.finPartialProduct_zero
Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · statement
theorem finPartialProduct_zero
    {C : Type*} [CommMonoid C] {n : ℕ}
    (v : Fin n → C) :
    finPartialProduct v 0 = 1
theorem

finPartialProduct_succ

L118 ↗
CyclicCohomology.finPartialProduct_succ
Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · statement
theorem finPartialProduct_succ
    {C : Type*} [CommMonoid C] {n : ℕ}
    (v : Fin n → C) (i : Fin n) :
    finPartialProduct v (i.1 + 1) =
      finPartialProduct v i.1 * v i
theorem

finPartialProduct_full

L126 ↗
CyclicCohomology.finPartialProduct_full
Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · statement
theorem finPartialProduct_full
    {C : Type*} [CommMonoid C] {n : ℕ}
    (v : Fin n → C) :
    finPartialProduct v n = ∏ i : Fin n, v i
def

quotientMulEquivOfSplit

L136 ↗
CyclicCohomology.quotientMulEquivOfSplit
Documentation

A split homomorphism induces an equivalence of quotients when it identifies the selected subgroups and its remaining kernel lies in the source subgroup.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · statement
def quotientMulEquivOfSplit
    {X Y : Type*} [CommGroup X] [CommGroup Y]
    (N : Subgroup X) (M : Subgroup Y)
    (f : X →* Y) (s : Y →* X)
    (hfs : ∀ y : Y, f (s y) = y)
    (hfN : ∀ x : X, x ∈ N → f x ∈ M)
    (hsM : ∀ y : Y, y ∈ M → s y ∈ N)
    (hker : ∀ x : X, f x = 1 → x ∈ N) :
    X ⧸ N ≃* Y ⧸ M
abbrev

inducedMulDistribMulAction

L165 ↗
CyclicCohomology.inducedMulDistribMulAction
Documentation

Compatibility name for the canonical action supplied by the common core. This alias is not registered as an additional instance.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · statement
abbrev inducedMulDistribMulAction [Group G] (H : Subgroup G) [CommGroup B]
    [MulDistribMulAction H B] :
    MulDistribMulAction G (InducedModule (B := B) H)
def

inducedFixedEquiv

L172 ↗
CyclicCohomology.inducedFixedEquiv
Documentation

Evaluation at the identity identifies the fixed points of an induced module with the fixed points for the inducing subgroup.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · full declaration
def inducedFixedEquiv [Group G] (H : Subgroup G)
    [CommGroup B] [MulDistribMulAction H B] :
    fixedSubgroup G (InducedModule (B := B) H) ≃*
      fixedSubgroup H B where
  toFun f := ⟨f.1.1 1, by
    intro h
    have hcov := f.1.2 h 1
    have hfix := congrArg
      (fun q : InducedModule (B := B) H ↦ q.1 1) (f.2 h.1)
    change f.1.1 (h.1 * 1) = h • f.1.1 1 at hcov
    change f.1.1 (1 * h.1) = f.1.1 1 at hfix
    have hcov' : h • f.1.1 1 = f.1.1 h.1 := by
      simpa using hcov.symm
    have hfix' : f.1.1 h.1 = f.1.1 1 := by
      simpa using hfix
    exact hcov'.trans hfix'⟩
  invFun b := ⟨⟨fun _ ↦ b.1, by
      intro h x
      exact (b.2 h).symm⟩,
    by
      intro g
      apply Subtype.ext
      funext x
      rfl⟩
  left_inv f := by
    apply Subtype.ext
    apply Subtype.ext
    funext x
    have hx := congrArg
      (fun q : InducedModule (B := B) H ↦ q.1 1) (f.2 x)
    change f.1.1 (1 * x) = f.1.1 1 at hx
    simpa using hx.symm
  right_inv b := by
    apply Subtype.ext
    rfl
  map_mul' _ _ := rfl
theorem

inducedFixedEquiv_apply_coe

L210 ↗
CyclicCohomology.inducedFixedEquiv_apply_coe
Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
Lean source · statement
theorem inducedFixedEquiv_apply_coe [Group G] (H : Subgroup G)
    [CommGroup B] [MulDistribMulAction H B]
    (f : fixedSubgroup G (InducedModule (B := B) H)) :
    (inducedFixedEquiv H f : B) = f.1.1 1
theorem

quotientGenerator_generates

L223 ↗
CyclicCohomology.quotientGenerator_generates
Documentation

A chosen generator of a finite cyclic group also generates its quotient by any subgroup.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section CyclicCoordinates
variable [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem quotientGenerator_generates (H : Subgroup G) (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    ∀ q : G ⧸ H, q ∈
      Subgroup.zpowers (QuotientGroup.mk' H σ)
theorem

quotientGenerator_order

L236 ↗
CyclicCohomology.quotientGenerator_order
Documentation

The image of a cyclic generator in G/H has order [G:H].

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section CyclicCoordinates
variable [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem quotientGenerator_order (H : Subgroup G) (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    orderOf (QuotientGroup.mk' H σ) = H.index
def

cyclicCosetEquiv

L245 ↗
CyclicCohomology.cyclicCosetEquiv
Documentation

The powers 1, σ, ..., σ^([G:H]-1) form the canonical transversal used in the cyclic induced-module calculation.

Source context 7 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section CyclicCoordinates
variable [CommGroup G] [Fintype G]
Lean source · statement
def cyclicCosetEquiv (H : Subgroup G) (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    H × Fin H.index ≃ G
theorem

cyclicCosetEquiv_apply

L306 ↗
CyclicCohomology.cyclicCosetEquiv_apply
Source context 7 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section CyclicCoordinates
variable [CommGroup G] [Fintype G]
Lean source · statement
theorem cyclicCosetEquiv_apply (H : Subgroup G) (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    (h : H) (i : Fin H.index) :
    cyclicCosetEquiv H σ hgen (h, i) =
      h.1 * σ ^ i.1
theorem

cyclic_pow_index_mem

L318 ↗
CyclicCohomology.cyclic_pow_index_mem
Documentation

The power σ^[G:H] belongs to H.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section CyclicCoordinates
variable [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem cyclic_pow_index_mem (H : Subgroup G) (σ : G) :
    σ ^ H.index ∈ H
theorem

zpowers_pow_index_eq

L324 ↗
CyclicCohomology.zpowers_pow_index_eq
Documentation

In a cyclic group, σ^[G:H] generates H.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section CyclicCoordinates
variable [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem zpowers_pow_index_eq [Finite G] (H : Subgroup G) (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    Subgroup.zpowers (σ ^ H.index) = H
def

subgroupGenerator

L352 ↗
CyclicCohomology.subgroupGenerator
Documentation

The canonical generator of H attached to σ.

Source context 7 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section CyclicCoordinates
variable [CommGroup G] [Fintype G]
Lean source · statement
def subgroupGenerator (H : Subgroup G) (σ : G) : H
theorem

subgroupGenerator_coe

L357 ↗
CyclicCohomology.subgroupGenerator_coe
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section CyclicCoordinates
variable [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem subgroupGenerator_coe (H : Subgroup G) (σ : G) :
    (subgroupGenerator H σ : G) = σ ^ H.index
theorem

subgroupGenerator_generates

L363 ↗
CyclicCohomology.subgroupGenerator_generates
Documentation

The canonical element σ^[G:H] generates H.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section CyclicCoordinates
variable [CommGroup G] [Fintype G]
omit [Fintype G] in
Lean source · statement
theorem subgroupGenerator_generates [Finite G] (H : Subgroup G) (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    ∀ h : H, h ∈ Subgroup.zpowers (subgroupGenerator H σ)
def

inducedCoordinates

L386 ↗
CyclicCohomology.inducedCoordinates
Documentation

Restriction to the canonical cyclic transversal identifies an induced module with a finite product of copies of the inducing group.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedCoordinates
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · full declaration
def inducedCoordinates (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    InducedModule (B := B) H ≃*
      (Fin H.index → B) where
  toFun f i := f.1 (σ ^ i.1)
  invFun v := ⟨fun x ↦
      let p := (cyclicCosetEquiv H σ hgen).symm x
      p.1 • v p.2,
    by
      intro h x
      let e := cyclicCosetEquiv H σ hgen
      let p := e.symm x
      have hp : p.1.1 * σ ^ p.2.1 = x := by
        have hx := e.apply_symm_apply x
        change p.1.1 * σ ^ p.2.1 = x at hx
        exact hx
      have hsymm :
          e.symm (h.1 * x) = (h * p.1, p.2) := by
        apply e.injective
        rw [e.apply_symm_apply]
        change h.1 * x =
          (h * p.1).1 * σ ^ p.2.1
        rw [← hp]
        simp only [Subgroup.coe_mul]
        exact (mul_assoc h.1 p.1.1
          (σ ^ p.2.1)).symm
      change
        (e.symm (h.1 * x)).1 •
            v (e.symm (h.1 * x)).2 =
          h • p.1 • v p.2
      rw [hsymm]
      exact mul_smul h p.1 (v p.2)⟩
  left_inv f := by
    apply Subtype.ext
    funext x
    let e := cyclicCosetEquiv H σ hgen
    let p := e.symm x
    have hp : p.1.1 * σ ^ p.2.1 = x := by
      have hx := e.apply_symm_apply x
      change p.1.1 * σ ^ p.2.1 = x at hx
      exact hx
    change p.1 • f.1 (σ ^ p.2.1) = f.1 x
    rw [← hp]
    exact (f.2 p.1 (σ ^ p.2.1)).symm
  right_inv v := by
    funext i
    let e := cyclicCosetEquiv H σ hgen
    have hsymm : e.symm (σ ^ i.1) = (1, i) := by
      apply e.injective
      simp [e]
    change
      (e.symm (σ ^ i.1)).1 •
          v (e.symm (σ ^ i.1)).2 = v i
    rw [hsymm]
    exact one_smul H (v i)
  map_mul' f k := by
    funext i
    rfl
theorem

inducedCoordinates_apply

L446 ↗
CyclicCohomology.inducedCoordinates_apply
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedCoordinates
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem inducedCoordinates_apply (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    (f : InducedModule (B := B) H)
    (i : Fin H.index) :
    inducedCoordinates H σ hgen f i =
      f.1 (σ ^ i.1)
def

inducedFirstCoordinateHom

L456 ↗
CyclicCohomology.inducedFirstCoordinateHom
Documentation

The multiplicative section supported on the first transversal coordinate.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedCoordinates
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · full declaration
def inducedFirstCoordinateHom :
    B →* (Fin H.index → B) where
  toFun b i := if i.1 = 0 then b else 1
  map_one' := by
    funext i
    split <;> rfl
  map_mul' b c := by
    funext i
    by_cases hi : i.1 = 0 <;> simp [hi]
def

inducedSection

L467 ↗
CyclicCohomology.inducedSection
Documentation

The canonical multiplicative section from the inducing group.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedCoordinates
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
def inducedSection (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    B →* InducedModule (B := B) H
theorem

inducedSection_apply_one

L474 ↗
CyclicCohomology.inducedSection_apply_one
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedCoordinates
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem inducedSection_apply_one (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) (b : B) :
    (inducedSection H σ hgen b).1 1 = b
def

inducedCoordinateProduct

L492 ↗
CyclicCohomology.inducedCoordinateProduct
Documentation

Product over the canonical transversal.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedCoordinates
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · full declaration
def inducedCoordinateProduct (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    InducedModule (B := B) H →* B where
  toFun f :=
    ∏ i : Fin H.index,
      inducedCoordinates H σ hgen f i
  map_one' := by simp
  map_mul' f k := by
    simp only [map_mul, Pi.mul_apply,
      Finset.prod_mul_distrib]
theorem

inducedCoordinateProduct_apply

L504 ↗
CyclicCohomology.inducedCoordinateProduct_apply
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedCoordinates
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem inducedCoordinateProduct_apply (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    (f : InducedModule (B := B) H) :
    inducedCoordinateProduct H σ hgen f =
      ∏ i : Fin H.index, f.1 (σ ^ i.1)
theorem

inducedCoordinateProduct_section

L514 ↗
CyclicCohomology.inducedCoordinateProduct_section
Documentation

The first-coordinate section is a right inverse to the transversal product.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedCoordinates
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
theorem inducedCoordinateProduct_section (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) (b : B) :
    inducedCoordinateProduct H σ hgen
        (inducedSection H σ hgen b) = b
instance

(anonymous instance)

L546 ↗
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandH0
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
instance : Fintype H
theorem

inducedEvaluation_tateNorm

L550 ↗
CyclicCohomology.inducedEvaluation_tateNorm
Documentation

Norm compatibility under evaluation: ev₁(N_G f) = N_H(∏_{G/H} f).

Source context 9 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandH0
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
Lean source · statement
theorem inducedEvaluation_tateNorm (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    (f : InducedModule (B := B) H) :
    inducedEvaluation H
        (tateNorm G (InducedModule (B := B) H) f) =
      tateNorm H B
        (inducedCoordinateProduct H σ hgen f)
theorem

inducedFixedEquiv_mem_tateNormSubgroup_iff

L610 ↗
CyclicCohomology.inducedFixedEquiv_mem_tateNormSubgroup_iff
Documentation

Under evaluation of fixed points, global and subgroup norm images correspond.

Source context 9 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandH0
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
Lean source · statement
theorem inducedFixedEquiv_mem_tateNormSubgroup_iff
    (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    (x : fixedSubgroup G
      (InducedModule (B := B) H)) :
    x.1 ∈ tateNormSubgroup G
        (InducedModule (B := B) H) ↔
      (inducedFixedEquiv H x).1 ∈
        tateNormSubgroup H B
def

inducedHerbrandH0Equiv

L665 ↗
CyclicCohomology.inducedHerbrandH0Equiv
Documentation

Multiplicative Shapiro lemma in Tate degree zero.

Source context 9 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandH0
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
Lean source · statement
def inducedHerbrandH0Equiv (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    HerbrandH0 G (InducedModule (B := B) H) ≃*
      HerbrandH0 H B
instance

(anonymous instance)

L710 ↗
Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
instance : Fintype H
instance

(anonymous instance)

L713 ↗
Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
omit [Fintype G] in
Lean source · statement
instance [Finite G] : NeZero H.index
theorem

inducedCoordinates_smul_generator

L719 ↗
CyclicCohomology.inducedCoordinates_smul_generator
Documentation

In canonical coordinates, right translation by σ is the cyclic shift whose wrap-around is acted on by σ^[G:H].

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · statement
theorem inducedCoordinates_smul_generator (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    (f : InducedModule (B := B) H)
    (i : Fin H.index) :
    inducedCoordinates H σ hgen (σ • f) i =
      twistedFinRotate (subgroupGenerator H σ)
        (inducedCoordinates H σ hgen f) i
theorem

inducedCoordinateProduct_sigmaMinusOne

L746 ↗
CyclicCohomology.inducedCoordinateProduct_sigmaMinusOne
Documentation

The transversal product sends a σ-coboundary to the corresponding σ^[G:H]-coboundary.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · statement
theorem inducedCoordinateProduct_sigmaMinusOne
    (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    (f : InducedModule (B := B) H) :
    inducedCoordinateProduct H σ hgen
        (sigmaMinusOne G
          (InducedModule (B := B) H) σ f) =
      sigmaMinusOne H B
        (subgroupGenerator H σ) (f.1 1)
theorem

inducedCoordinateProduct_eq_one_mem_augmentation

L794 ↗
CyclicCohomology.inducedCoordinateProduct_eq_one_mem_augmentation
Documentation

If the product of the canonical coordinates is one, successive partial products construct a σ-primitive.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · statement
theorem inducedCoordinateProduct_eq_one_mem_augmentation
    (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    (f : InducedModule (B := B) H)
    (hf :
      inducedCoordinateProduct H σ hgen f = 1) :
    f ∈ augmentationSubgroup G
      (InducedModule (B := B) H) σ
theorem

inducedCoordinateProduct_mem_normKernel

L879 ↗
CyclicCohomology.inducedCoordinateProduct_mem_normKernel
Documentation

The transversal product carries the ambient norm kernel into the subgroup norm kernel.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · statement
theorem inducedCoordinateProduct_mem_normKernel
    (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    {f : InducedModule (B := B) H}
    (hf : f ∈ normKernelSubgroup G
      (InducedModule (B := B) H)) :
    inducedCoordinateProduct H σ hgen f ∈
      normKernelSubgroup H B
theorem

inducedSection_mem_normKernel

L906 ↗
CyclicCohomology.inducedSection_mem_normKernel
Documentation

The canonical section carries the subgroup norm kernel into the ambient norm kernel.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · statement
theorem inducedSection_mem_normKernel (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    {b : B} (hb : b ∈ normKernelSubgroup H B) :
    inducedSection H σ hgen b ∈
      normKernelSubgroup G
        (InducedModule (B := B) H)
theorem

inducedCoordinateProduct_mem_augmentation

L939 ↗
CyclicCohomology.inducedCoordinateProduct_mem_augmentation
Documentation

The transversal product maps augmentation subgroups compatibly.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · statement
theorem inducedCoordinateProduct_mem_augmentation
    (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    {f : InducedModule (B := B) H}
    (hf : f ∈ augmentationSubgroup G
      (InducedModule (B := B) H) σ) :
    inducedCoordinateProduct H σ hgen f ∈
      augmentationSubgroup H B
        (subgroupGenerator H σ)
theorem

inducedSection_mem_augmentation

L956 ↗
CyclicCohomology.inducedSection_mem_augmentation
Documentation

The canonical section maps subgroup coboundaries to ambient coboundaries.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · statement
theorem inducedSection_mem_augmentation (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ)
    {b : B}
    (hb : b ∈ augmentationSubgroup H B
      (subgroupGenerator H σ)) :
    inducedSection H σ hgen b ∈
      augmentationSubgroup G
        (InducedModule (B := B) H) σ
def

inducedNormKernelProductHom

L1024 ↗
CyclicCohomology.inducedNormKernelProductHom
Documentation

Restriction of the transversal product to 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 uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · full declaration
def inducedNormKernelProductHom (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    normKernelSubgroup G
        (InducedModule (B := B) H) →*
      normKernelSubgroup H B where
  toFun f :=
    ⟨inducedCoordinateProduct H σ hgen f.1,
      inducedCoordinateProduct_mem_normKernel
        H σ hgen f.2⟩
  map_one' := by
    apply Subtype.ext
    exact map_one
      (inducedCoordinateProduct H σ hgen)
  map_mul' x y := by
    apply Subtype.ext
    exact map_mul
      (inducedCoordinateProduct H σ hgen)
        x.1 y.1
def

inducedNormKernelSectionHom

L1044 ↗
CyclicCohomology.inducedNormKernelSectionHom
Documentation

Restriction of the canonical section to 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 uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · full declaration
def inducedNormKernelSectionHom (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    normKernelSubgroup H B →*
      normKernelSubgroup G
        (InducedModule (B := B) H) where
  toFun b :=
    ⟨inducedSection H σ hgen b.1,
      inducedSection_mem_normKernel
        H σ hgen b.2⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (inducedSection H σ hgen)
  map_mul' x y := by
    apply Subtype.ext
    exact map_mul (inducedSection H σ hgen)
      x.1 y.1
def

inducedHerbrandHMinusOneEquiv

L1062 ↗
CyclicCohomology.inducedHerbrandHMinusOneEquiv
Documentation

Multiplicative Shapiro lemma in Tate degree minus one.

Source context 10 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section InducedHerbrandHMinusOne
variable [CommGroup G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
local instance : Fintype H := Fintype.ofFinite H
local instance [Finite G] : NeZero H.index := ⟨by
  rw [H.index_eq_card]
  exact Nat.card_pos.ne'⟩
Lean source · statement
def inducedHerbrandHMinusOneEquiv
    (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    HerbrandHMinusOne G
        (InducedModule (B := B) H) σ ≃*
      HerbrandHMinusOne H B
        (subgroupGenerator H σ)
def

subgroupGeneratorOfGenerator

L1119 ↗
CyclicCohomology.subgroupGeneratorOfGenerator
Documentation

The canonical generator of a subgroup, exposed without requiring a global CommGroup G instance. Commutativity is derived from the supplied cyclic generator.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section FiniteCyclicGroup
variable [Group G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
def subgroupGeneratorOfGenerator (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) : H
theorem

subgroupGeneratorOfGenerator_coe

L1127 ↗
CyclicCohomology.subgroupGeneratorOfGenerator_coe
Source context 9 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section FiniteCyclicGroup
variable [Group G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
omit [Fintype G] in
Lean source · statement
theorem subgroupGeneratorOfGenerator_coe (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    (subgroupGeneratorOfGenerator H σ hgen : G) =
      σ ^ H.index
theorem

subgroupGeneratorOfGenerator_generates

L1135 ↗
CyclicCohomology.subgroupGeneratorOfGenerator_generates
Documentation

The derived element σ^[G:H] generates H.

Source context 9 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section FiniteCyclicGroup
variable [Group G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
omit [Fintype G] in
Lean source · statement
theorem subgroupGeneratorOfGenerator_generates [Finite G] (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    ∀ h : H,
      h ∈ Subgroup.zpowers
        (subgroupGeneratorOfGenerator H σ hgen)
def

inducedCoordinatesOfFiniteCyclic

L1150 ↗
CyclicCohomology.inducedCoordinatesOfFiniteCyclic
Documentation

Cyclic-transversal coordinates for an ordinary finite cyclic group.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section FiniteCyclicGroup
variable [Group G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · statement
def inducedCoordinatesOfFiniteCyclic
    (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    InducedModule (B := B) H ≃*
      (Fin H.index → B)
def

inducedHerbrandH0EquivOfFiniteCyclic

L1161 ↗
CyclicCohomology.inducedHerbrandH0EquivOfFiniteCyclic
Documentation

Tate-degree-zero Shapiro equivalence for an ordinary finite cyclic group.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section FiniteCyclicGroup
variable [Group G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · full declaration
def inducedHerbrandH0EquivOfFiniteCyclic
    (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    letI : Fintype H := Fintype.ofFinite H
    HerbrandH0 G (InducedModule (B := B) H) ≃*
      HerbrandH0 H B := by
  letI : Fintype H := Fintype.ofFinite H
  letI : IsCyclic G := ⟨⟨σ, hgen⟩⟩
  letI : CommGroup G := IsCyclic.commGroup
  exact inducedHerbrandH0Equiv H σ hgen
def

inducedHerbrandHMinusOneEquivOfFiniteCyclic

L1174 ↗
CyclicCohomology.inducedHerbrandHMinusOneEquivOfFiniteCyclic
Documentation

Tate-degree-minus-one Shapiro equivalence for an ordinary finite cyclic group.

Source context 8 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uB
variable {G : Type uG} {B : Type uB}
section FiniteCyclicGroup
variable [Group G] [Fintype G] [CommGroup B]
variable (H : Subgroup G) [MulDistribMulAction H B]
Lean source · full declaration
def inducedHerbrandHMinusOneEquivOfFiniteCyclic
    (σ : G)
    (hgen : ∀ x : G, x ∈ Subgroup.zpowers σ) :
    letI : Fintype H := Fintype.ofFinite H
    HerbrandHMinusOne G
        (InducedModule (B := B) H) σ ≃*
      HerbrandHMinusOne H B
        (subgroupGeneratorOfGenerator H σ hgen) := by
  letI : Fintype H := Fintype.ofFinite H
  letI : IsCyclic G := ⟨⟨σ, hgen⟩⟩
  letI : CommGroup G := IsCyclic.commGroup
  have hτ :
      subgroupGeneratorOfGenerator H σ hgen =
        subgroupGenerator H σ :=
    Subtype.ext (by rfl)
  rw [hτ]
  exact inducedHerbrandHMinusOneEquiv H σ hgen

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