NYLL
Module

EquivariantEquiv.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.EquivariantEquiv
10 declarations indexed from sourceView source ↗

Module documentation

Low-degree Tate cohomology under equivariant equivalences

An equivariant multiplicative equivalence identifies fixed elements, norm kernels, norm images, and augmentation images. Consequently it induces equivalences on the concrete low-degree Tate cohomology groups and preserves the Herbrand quotient.

These transport results let calculations made on field units or local coordinates be applied to their actual images inside idele groups without introducing comparison assumptions.

Imports3
Imported by7

Declarations

theorem

equivariantMulEquiv_map_tateNorm

L42 ↗
CyclicCohomology.equivariantMulEquiv_map_tateNorm
Documentation

An equivariant multiplicative equivalence commutes with the finite group norm.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
Lean source · statement
theorem equivariantMulEquiv_map_tateNorm
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a)
    (a : A) :
    e (tateNorm G A a) =
      tateNorm G B (e a)
theorem

equivariantMulEquiv_map_sigmaMinusOne

L58 ↗
CyclicCohomology.equivariantMulEquiv_map_sigmaMinusOne
Documentation

An equivariant multiplicative equivalence commutes with the augmentation operator.

Source context 6 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
omit [Fintype G] in
Lean source · statement
theorem equivariantMulEquiv_map_sigmaMinusOne
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a)
    (σ : G) (a : A) :
    e (sigmaMinusOne G A σ a) =
      sigmaMinusOne G B σ (e a)
def

fixedSubgroupEquivariantMulEquiv

L73 ↗
CyclicCohomology.fixedSubgroupEquivariantMulEquiv
Documentation

An equivariant multiplicative equivalence restricted to fixed subgroups.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
Lean source · full declaration
def fixedSubgroupEquivariantMulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a) :
    fixedSubgroup G A ≃* fixedSubgroup G B where
  toFun a :=
    ⟨e a.1, fun g ↦ by
      rw [← he g a.1, a.2 g]⟩
  invFun b :=
    ⟨e.symm b.1, fun g ↦ by
      rw [← mulEquiv_symm_commutes_smul e he, b.2 g]⟩
  left_inv a := by
    apply Subtype.ext
    exact e.symm_apply_apply a.1
  right_inv b := by
    apply Subtype.ext
    exact e.apply_symm_apply b.1
  map_mul' _ _ := by
    apply Subtype.ext
    exact e.map_mul _ _
def

normKernelEquivariantMulEquiv

L96 ↗
CyclicCohomology.normKernelEquivariantMulEquiv
Documentation

An equivariant multiplicative equivalence restricted to norm kernels.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
Lean source · full declaration
def normKernelEquivariantMulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a) :
    normKernelSubgroup G A ≃*
      normKernelSubgroup G B where
  toFun a :=
    ⟨e a.1, by
      change tateNorm G B (e a.1) = 1
      calc
        tateNorm G B (e a.1) =
            e (tateNorm G A a.1) :=
          (equivariantMulEquiv_map_tateNorm
            e he a.1).symm
        _ = e 1 := congrArg e a.2
        _ = 1 := e.map_one⟩
  invFun b :=
    ⟨e.symm b.1, by
      change tateNorm G A (e.symm b.1) = 1
      apply e.injective
      calc
        e (tateNorm G A (e.symm b.1)) =
            tateNorm G B (e (e.symm b.1)) :=
          equivariantMulEquiv_map_tateNorm
            e he (e.symm b.1)
        _ = tateNorm G B b.1 := by
          rw [e.apply_symm_apply]
        _ = 1 := b.2
        _ = e 1 := e.map_one.symm⟩
  left_inv a := by
    apply Subtype.ext
    exact e.symm_apply_apply a.1
  right_inv b := by
    apply Subtype.ext
    exact e.apply_symm_apply b.1
  map_mul' _ _ := by
    apply Subtype.ext
    exact e.map_mul _ _
def

herbrandH0EquivariantMulEquiv

L137 ↗
CyclicCohomology.herbrandH0EquivariantMulEquiv
Documentation

An equivariant multiplicative equivalence induces an equivalence on degree-zero Tate cohomology.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
Lean source · statement
def herbrandH0EquivariantMulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a) :
    HerbrandH0 G A ≃* HerbrandH0 G B
theorem

herbrandH0EquivariantMulEquiv_mk

L189 ↗
CyclicCohomology.herbrandH0EquivariantMulEquiv_mk
Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
Lean source · statement
theorem herbrandH0EquivariantMulEquiv_mk
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a)
    (a : fixedSubgroup G A) :
    herbrandH0EquivariantMulEquiv e he (HerbrandH0.mk a) =
      HerbrandH0.mk (fixedSubgroupEquivariantMulEquiv e he a)
def

herbrandHMinusOneEquivariantMulEquiv

L200 ↗
CyclicCohomology.herbrandHMinusOneEquivariantMulEquiv
Documentation

An equivariant multiplicative equivalence induces an equivalence on degree-minus-one Tate cohomology.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
Lean source · statement
def herbrandHMinusOneEquivariantMulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a)
    (σ : G) :
    HerbrandHMinusOne G A σ ≃*
      HerbrandHMinusOne G B σ
theorem

herbrandH0Finite_of_equivariantMulEquiv

L255 ↗
CyclicCohomology.herbrandH0Finite_of_equivariantMulEquiv
Documentation

Finiteness of H⁰ transports through an equivariant multiplicative equivalence.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
Lean source · statement
theorem herbrandH0Finite_of_equivariantMulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a)
    [Finite (HerbrandH0 G A)] :
    Finite (HerbrandH0 G B)
theorem

herbrandHMinusOneFinite_of_equivariantMulEquiv

L267 ↗
CyclicCohomology.herbrandHMinusOneFinite_of_equivariantMulEquiv
Documentation

Finiteness of H⁻¹ transports through an equivariant multiplicative equivalence.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
Lean source · statement
theorem herbrandHMinusOneFinite_of_equivariantMulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a)
    (σ : G)
    [Finite (HerbrandHMinusOne G A σ)] :
    Finite (HerbrandHMinusOne G B σ)
theorem

herbrandQuotient_eq_of_equivariantMulEquiv

L281 ↗
CyclicCohomology.herbrandQuotient_eq_of_equivariantMulEquiv
Documentation

Herbrand quotients are invariant under equivariant multiplicative equivalence.

Source context 5 commands

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

noncomputable section
namespace CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
universe uG uA uB
variable {G : Type uG} {A : Type uA} {B : Type uB}
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B]
    [MulDistribMulAction G A]
    [MulDistribMulAction G B]
Lean source · full declaration
theorem herbrandQuotient_eq_of_equivariantMulEquiv
    (e : A ≃* B)
    (he : ∀ (g : G) (a : A),
      e (g • a) = g • e a)
    (σ : G)
    [Finite (HerbrandH0 G A)]
    [Finite (HerbrandHMinusOne G A σ)] :
    letI _h0B : Finite (HerbrandH0 G B) :=
      herbrandH0Finite_of_equivariantMulEquiv e he
    letI _hMinusOneB :
        Finite (HerbrandHMinusOne G B σ) :=
      herbrandHMinusOneFinite_of_equivariantMulEquiv
        e he σ
    herbrandQuotient (G := G) (A := A) σ =
      herbrandQuotient (G := G) (A := B) σ := by
  let h0B : Finite (HerbrandH0 G B) :=
    herbrandH0Finite_of_equivariantMulEquiv e he
  let hMinusOneB :
      Finite (HerbrandHMinusOne G B σ) :=
    herbrandHMinusOneFinite_of_equivariantMulEquiv
      e he σ
  have h0Card :
      Nat.card (HerbrandH0 G A) =
        Nat.card (HerbrandH0 G B) := by
    exact Nat.card_congr
      (herbrandH0EquivariantMulEquiv e he).toEquiv
  have hMinusOneCard :
      Nat.card (HerbrandHMinusOne G A σ) =
        Nat.card
          (HerbrandHMinusOne G B σ) := by
    exact Nat.card_congr
      (herbrandHMinusOneEquivariantMulEquiv
        e he σ).toEquiv
  rw [herbrandQuotient_eq_card_ratio,
    herbrandQuotient_eq_card_ratio,
    h0Card, hMinusOneCard]

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