NYLL
Module

Cardinality.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.Cardinality
21 declarations indexed from sourceView source ↗

Module documentation

Cardinality identity from the standard Tate exact sequence

For a short exact sequence of finite cyclic modules, this module applies mathlib's homology long exact sequence to the standard two-periodic cyclic complex. The resulting cardinality identity is transported to the arithmetic H⁰ and H⁻¹ presentations.

Imports2
Imported by3

Declarations

def

subCompNormMap

L37 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.subCompNormMap
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · full declaration
def subCompNormMap
    (σ : G) (f : A →* B)
    (hf : ∀ (g : G) (a : A), f (g • a) = g • f a) :
    Rep.FiniteCyclicGroup.subCompNormHom
        (Rep.ofMulDistribMulAction G A) σ ⟶
      Rep.FiniteCyclicGroup.subCompNormHom
        (Rep.ofMulDistribMulAction G B) σ where
  τ₁ := (equivariantRepHom f hf).toModuleCatHom
  τ₂ := (equivariantRepHom f hf).toModuleCatHom
  τ₃ := (equivariantRepHom f hf).toModuleCatHom
  comm₁₂ := by
    ext a
    change Additive A at a
    change
      Additive.ofMul ((σ • f a.toMul) / f a.toMul) =
        Additive.ofMul (f ((σ • a.toMul) / a.toMul))
    exact congrArg Additive.ofMul (by rw [map_div, hf])
  comm₂₃ := by
    ext a
    apply Additive.ofMul.injective
    simp [Rep.FiniteCyclicGroup.subCompNormHom, Rep.norm,
      Representation.norm, Rep.hom_comm_apply]
def

periodicChainMap

L60 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicChainMap
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · full declaration
def periodicChainMap
    (σ : G) (f : A →* B)
    (hf : ∀ (g : G) (a : A), f (g • a) = g • f a) :
    Rep.FiniteCyclicGroup.moduleCatChainComplex
        (Rep.ofMulDistribMulAction G A) σ ⟶
      Rep.FiniteCyclicGroup.moduleCatChainComplex
        (Rep.ofMulDistribMulAction G B) σ where
  f _ := (equivariantRepHom f hf).toModuleCatHom
  comm' := by
    rintro i j ⟨rfl⟩
    have hrel : (ComplexShape.down ℕ).Rel (j + 1) j := rfl
    by_cases hj : Even (j + 1)
    · simp only [Rep.FiniteCyclicGroup.moduleCatChainComplex,
        HomologicalComplex.alternatingConst, dite_eq_ite, hrel, hj, ↓reduceIte]
      exact (subCompNormMap σ f hf).comm₂₃
    · simp only [Rep.FiniteCyclicGroup.moduleCatChainComplex,
        HomologicalComplex.alternatingConst, dite_eq_ite, hrel, hj, ↓reduceIte]
      exact (subCompNormMap σ f hf).comm₁₂
def

periodicShortComplex

L79 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicShortComplex
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
def periodicShortComplex
    (σ : G)
    (i : A →* B) (j : B →* C)
    (hi : ∀ (g : G) (a : A), i (g • a) = g • i a)
    (hj : ∀ (g : G) (b : B), j (g • b) = g • j b)
    (hker : ∀ b : B, j b = 1 ↔ ∃ a : A, i a = b) :
    ShortComplex (ChainComplex (ModuleCat ℤ) ℕ)
theorem

periodicShortComplex_shortExact

L94 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicShortComplex_shortExact
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem periodicShortComplex_shortExact
    (σ : G)
    (i : A →* B) (j : B →* C)
    (hi : ∀ (g : G) (a : A), i (g • a) = g • i a)
    (hj : ∀ (g : G) (b : B), j (g • b) = g • j b)
    (hker : ∀ b : B, j b = 1 ↔ ∃ a : A, i a = b)
    (hinj : Function.Injective i) (hsurj : Function.Surjective j) :
    (periodicShortComplex σ i j hi hj hker).ShortExact
def

periodicScIsoEven

L126 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicScIsoEven
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
def periodicScIsoEven
    {R H : Type} [CommRing R] [CommGroup H] [Fintype H]
    (M : Rep R H) (τ : H)
    {n : ℕ} [h₀ : NeZero n] (hn : Even n) :
    (Rep.FiniteCyclicGroup.moduleCatChainComplex M τ).sc n ≅
      Rep.FiniteCyclicGroup.subCompNormHom M τ
def

periodicScIsoOdd

L144 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicScIsoOdd
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
def periodicScIsoOdd
    {R H : Type} [CommRing R] [CommGroup H] [Fintype H]
    (M : Rep R H) (τ : H) {n : ℕ} (hn : Odd n) :
    (Rep.FiniteCyclicGroup.moduleCatChainComplex M τ).sc n ≅
      Rep.FiniteCyclicGroup.normHomCompSub M τ
def

periodicHomologyIsoEven

L158 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicHomologyIsoEven
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
def periodicHomologyIsoEven
    {R H : Type} [CommRing R] [CommGroup H] [Fintype H]
    (M : Rep R H) (τ : H)
    {n : ℕ} [NeZero n] (hn : Even n) :
    (Rep.FiniteCyclicGroup.moduleCatChainComplex M τ).homology n ≅
      (Rep.FiniteCyclicGroup.subCompNormHom M τ).homology
def

periodicHomologyIsoOdd

L166 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicHomologyIsoOdd
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
def periodicHomologyIsoOdd
    {R H : Type} [CommRing R] [CommGroup H] [Fintype H]
    (M : Rep R H) (τ : H) {n : ℕ} (hn : Odd n) :
    (Rep.FiniteCyclicGroup.moduleCatChainComplex M τ).homology n ≅
      (Rep.FiniteCyclicGroup.normHomCompSub M τ).homology
def

periodicEvenHerbrandHMinusOneIso

L173 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicEvenHerbrandHMinusOneIso
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
def periodicEvenHerbrandHMinusOneIso
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    {n : ℕ} [NeZero n] (hn : Even n) :
    (Rep.FiniteCyclicGroup.moduleCatChainComplex
        (Rep.ofMulDistribMulAction G A) σ).homology n ≅
      ModuleCat.of ℤ (Additive (HerbrandHMinusOne G A σ))
def

periodicOddHerbrandHZeroIso

L184 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicOddHerbrandHZeroIso
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
def periodicOddHerbrandHZeroIso
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    {n : ℕ} (hn : Odd n) :
    (Rep.FiniteCyclicGroup.moduleCatChainComplex
        (Rep.ofMulDistribMulAction G A) σ).homology n ≅
      ModuleCat.of ℤ (Additive (HerbrandH0 G A))
theorem

periodicScIsoEven_naturality

L195 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicScIsoEven_naturality
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem periodicScIsoEven_naturality
    (σ : G) {n : ℕ} [NeZero n] (hn : Even n)
    (f : A →* B)
    (hf : ∀ (g : G) (a : A), f (g • a) = g • f a) :
    ShortComplex.homologyMap
          (periodicScIsoEven
            (Rep.ofMulDistribMulAction G A) σ hn).inv ≫
        ShortComplex.homologyMap
          ((HomologicalComplex.shortComplexFunctor
            (ModuleCat ℤ) (ComplexShape.down ℕ) n).map
              (periodicChainMap σ f hf)) ≫
        ShortComplex.homologyMap
          (periodicScIsoEven
            (Rep.ofMulDistribMulAction G B) σ hn).hom =
      ShortComplex.homologyMap (subCompNormMap σ f hf)
theorem

periodicHomologyIsoEven_naturality

L213 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.periodicHomologyIsoEven_naturality
Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem periodicHomologyIsoEven_naturality
    (σ : G) {n : ℕ} [NeZero n] (hn : Even n)
    (f : A →* B)
    (hf : ∀ (g : G) (a : A), f (g • a) = g • f a) :
    (periodicHomologyIsoEven
      (Rep.ofMulDistribMulAction G A) σ hn).inv ≫
        HomologicalComplex.homologyMap (periodicChainMap σ f hf) n ≫
        (periodicHomologyIsoEven
          (Rep.ofMulDistribMulAction G B) σ hn).hom =
      ShortComplex.homologyMap (subCompNormMap σ f hf)
def

moduleCatRangeEquivOfConjugate

L227 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.moduleCatRangeEquivOfConjugate
Documentation

Conjugating a ModuleCat ℤ morphism by isomorphisms identifies the ranges of the associated multiplicatively tagged homomorphisms.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
def moduleCatRangeEquivOfConjugate
    {X Y X' Y' : ModuleCat.{0} ℤ}
    (f : X ⟶ Y) (g : X' ⟶ Y')
    (eX : X ≅ X') (eY : Y ≅ Y')
    (h : eX.inv ≫ f ≫ eY.hom = g) :
    MonoidHom.range f.hom.toAddMonoidHom.toMultiplicative ≃
      MonoidHom.range g.hom.toAddMonoidHom.toMultiplicative
theorem

moduleCatRangeCard_eq_of_conjugate

L272 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.moduleCatRangeCard_eq_of_conjugate
Documentation

Conjugate ModuleCat ℤ morphisms have ranges of the same cardinality after multiplicatively tagging their underlying additive groups.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem moduleCatRangeCard_eq_of_conjugate
    {X Y X' Y' : ModuleCat.{0} ℤ}
    (f : X ⟶ Y) (g : X' ⟶ Y')
    (eX : X ≅ X') (eY : Y ≅ Y')
    (h : eX.inv ≫ f ≫ eY.hom = g) :
    Nat.card (MonoidHom.range
        f.hom.toAddMonoidHom.toMultiplicative) =
      Nat.card (MonoidHom.range
        g.hom.toAddMonoidHom.toMultiplicative)
theorem

mulExact_of_moduleCat_exact

L285 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.mulExact_of_moduleCat_exact
Documentation

Function exactness of morphisms in ModuleCat ℤ gives multiplicative exactness after tagging the underlying additive groups as multiplicative.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem mulExact_of_moduleCat_exact
    {X Y Z : ModuleCat.{0} ℤ} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hexact : Function.Exact f g) :
    Function.MulExact
      f.hom.toAddMonoidHom.toMultiplicative
      g.hom.toAddMonoidHom.toMultiplicative
theorem

mulExact_of_moduleCat_shortComplex_exact

L305 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.mulExact_of_moduleCat_shortComplex_exact
Documentation

Exactness of a short complex in ModuleCat ℤ gives multiplicative exactness of its two underlying homomorphisms.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem mulExact_of_moduleCat_shortComplex_exact
    {X Y Z : ModuleCat.{0} ℤ} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hzero : f ≫ g = 0)
    (hexact : (ShortComplex.mk f g hzero).Exact) :
    Function.MulExact
      f.hom.toAddMonoidHom.toMultiplicative
      g.hom.toAddMonoidHom.toMultiplicative
theorem

moduleCat_card_eq_card_range_mul_card_range_of_exact

L318 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.moduleCat_card_eq_card_range_mul_card_range_of_exact
Documentation

For an exact pair of ModuleCat ℤ morphisms with finite middle term, the cardinality of the middle term is the product of the two range cardinalities.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem moduleCat_card_eq_card_range_mul_card_range_of_exact
    {X Y Z : ModuleCat.{0} ℤ} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hexact : Function.Exact f g) [Finite Y] :
    Nat.card Y =
      Nat.card (MonoidHom.range
        f.hom.toAddMonoidHom.toMultiplicative) *
      Nat.card (MonoidHom.range
        g.hom.toAddMonoidHom.toMultiplicative)
theorem

finite_source_of_moduleIso

L334 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.finite_source_of_moduleIso
Documentation

Finiteness transports from the target to the source of a ModuleCat ℤ isomorphism.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem finite_source_of_moduleIso
    {X Y : ModuleCat.{0} ℤ} (e : X ≅ Y) [Finite Y] :
    Finite X
theorem

finite_target_of_moduleIso

L342 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.finite_target_of_moduleIso
Documentation

Finiteness transports from the source to the target of a ModuleCat ℤ isomorphism.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem finite_target_of_moduleIso
    {X Y : ModuleCat.{0} ℤ} (e : X ≅ Y) [Finite X] :
    Finite Y
theorem

moduleCat_card_eq_of_iso

L350 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.moduleCat_card_eq_of_iso
Documentation

A ModuleCat ℤ isomorphism with the additive form of a commutative group identifies their cardinalities.

Source context 10 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
section
variable [CommGroup G] [Fintype G]
variable [CommGroup A] [CommGroup B] [CommGroup C]
variable [MulDistribMulAction G A] [MulDistribMulAction G B]
  [MulDistribMulAction G C]
Lean source · statement
theorem moduleCat_card_eq_of_iso
    {X : ModuleCat.{0} ℤ} {T : Type} [CommGroup T]
    (e : X ≅ ModuleCat.of ℤ (Additive T)) :
    Nat.card X = Nat.card T
theorem

herbrand_exact_cardinality_identity

L360 ↗
CyclicCohomology.ProfiniteCohomology.Herbrand.herbrand_exact_cardinality_identity
Documentation

The finite-cardinality identity supplied directly by mathlib's standard two-periodic Tate exact sequence for a finite cyclic group.

Source context 6 commands

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

namespace CyclicCohomology
noncomputable section
namespace ProfiniteCohomology
namespace Herbrand
open CategoryTheory
variable {G A B C : Type}
Lean source · statement
theorem herbrand_exact_cardinality_identity
    [Group G] [Fintype G]
    [CommGroup A] [CommGroup B] [CommGroup C]
    [MulDistribMulAction G A] [MulDistribMulAction G B]
    [MulDistribMulAction G C]
    (i : A →* B) (j : B →* C)
    (hi : ∀ (g : G) (a : A), i (g • a) = g • i a)
    (hj : ∀ (g : G) (b : B), j (g • b) = g • j b)
    (hker : ∀ b : B, j b = 1 ↔ ∃ a : A, i a = b)
    (hinj : Function.Injective i)
    (hsurj : ∀ c : C, ∃ b : B, j b = c)
    (σ : G) (hgen : ∀ g : G, g ∈ Subgroup.zpowers σ)
    [Finite (HerbrandH0 G A)] [Finite (HerbrandHMinusOne G A σ)]
    [Finite (HerbrandH0 G B)] [Finite (HerbrandHMinusOne G B σ)]
    [Finite (HerbrandH0 G C)] [Finite (HerbrandHMinusOne G C σ)] :
    Nat.card (HerbrandH0 G B) *
        Nat.card (HerbrandHMinusOne G A σ) *
        Nat.card (HerbrandHMinusOne G C σ) =
      Nat.card (HerbrandH0 G A) *
        Nat.card (HerbrandH0 G C) *
        Nat.card (HerbrandHMinusOne G B σ)

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