Module

IdentityAugmentation.lean

Nyll.ProCGroups.FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation

43 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — kernel boundary — identity augmentation

The principal declarations in this module are:

coinvariantsLEquivOfSubsingleton

For a representation of a subsingleton monoid, taking coinvariants does not change the underlying module.

rightRegularRepresentation

The right-regular \(\mathbb{Z}\)-linear representation on \(\mathbb{Z}[H]\), given by right multiplication by \(g^{-1}\). This is the representation whose low-degree group homology matches the identity-case Crowell relations.

rightRegularRepresentation_apply_single

The right-regular representation sends a single group element to the corresponding basis action.

rightRegularRepresentation_apply_of

The right-regular representation has the displayed value on a representative.

Imports3

Nyll.ProCGroups.FoxDifferential.Discrete.GroupRing
Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro

Imported by2

def

coinvariantsLEquivOfSubsingleton

L43 ↗

FoxDifferential.coinvariantsLEquivOfSubsingleton

Documentation

For a representation of a subsingleton monoid, taking coinvariants does not change the underlying module.

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]

Lean source · statement

def coinvariantsLEquivOfSubsingleton
    {k G V : Type*} [CommRing k] [Monoid G] [Subsingleton G]
    [AddCommGroup V] [Module k V] (ρ : Representation k G V) :
    Representation.Coinvariants ρ ≃ₗ[k] V

def

rightRegularRepresentation

L69 ↗

FoxDifferential.rightRegularRepresentation

Documentation

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]

Lean source · full declaration

def rightRegularRepresentation : Representation ℤ H (GroupRing H) where
  toFun g :=
    { toFun := fun x => x * MonoidAlgebra.of ℤ H g⁻¹
      map_add' := by
        intro x y
        simp only [MonoidAlgebra.of_apply, add_mul]
      map_smul' := by
        intro n x
        simpa using smul_mul_assoc n x (MonoidAlgebra.of ℤ H g⁻¹) }
  map_one' := by
    ext x
    simp only [inv_one, MonoidAlgebra.of_apply, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk,
  Function.comp_apply, MonoidAlgebra.lsingle_apply, MonoidAlgebra.single_mul_single, mul_one,
      Module.End.one_apply]
  map_mul' g₁ g₂ := by
    ext x
    simp only [mul_inv_rev, MonoidAlgebra.of_apply, LinearMap.coe_comp, LinearMap.coe_mk,
        AddHom.coe_mk,
  Function.comp_apply, MonoidAlgebra.lsingle_apply, MonoidAlgebra.single_mul_single, mul_one,
      Module.End.mul_apply,
  mul_assoc]

theorem

rightRegularRepresentation_apply_single

L96 ↗

FoxDifferential.rightRegularRepresentation_apply_single

Documentation

The right-regular representation sends a single group element to the corresponding basis action.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
omit [DecidableEq H] in

Lean source · statement

theorem rightRegularRepresentation_apply_single (g h : H) (n : ℤ) :
    rightRegularRepresentation H g (MonoidAlgebra.single h n) =
      MonoidAlgebra.single (h * g⁻¹) n

theorem

rightRegularRepresentation_apply_of

L106 ↗

FoxDifferential.rightRegularRepresentation_apply_of

Documentation

The right-regular representation has the displayed value on a representative.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
omit [DecidableEq H] in

Lean source · statement

theorem rightRegularRepresentation_apply_of (g h : H) :
    rightRegularRepresentation H g (MonoidAlgebra.of ℤ H h : GroupRing H) =
      MonoidAlgebra.of ℤ H (h * g⁻¹)

abbrev

rightRegularRep

L112 ↗

FoxDifferential.rightRegularRep

Documentation

The right-regular representation as an object of Rep \(\mathbb{Z}\) H.

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]

Lean source · statement

abbrev rightRegularRep : Rep ℤ H

theorem

rightRegular_d₂₁_single

L119 ↗

FoxDifferential.rightRegular_d₂₁_single

Documentation

The Crowell identity relations are precisely the \(d_{21}\)-images of the right-regular representation, on basis elements.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
omit [DecidableEq H] in

Lean source · statement

theorem rightRegular_d₂₁_single (g₁ g₂ : H) (r : GroupRing H) :
    groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single (g₁, g₂) r) =
      (-r) • relationElement (MonoidHom.id H) g₁ g₂

theorem

relationElement_eq_rightRegular_d₂₁_single

L132 ↗

FoxDifferential.relationElement_eq_rightRegular_d₂₁_single

Documentation

Rewriting the right-regular boundary identity in the Crowell direction.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
omit [DecidableEq H] in

Lean source · statement

theorem relationElement_eq_rightRegular_d₂₁_single (g₁ g₂ : H) (r : GroupRing H) :
    r • relationElement (MonoidHom.id H) g₁ g₂ =
      groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single (g₁, g₂) (-r))

theorem

rightRegular_d₂₁_mem_relationSubmodule

L140 ↗

FoxDifferential.rightRegular_d₂₁_mem_relationSubmodule

Documentation

Every right-regular 1-boundary is a Crowell relation in the identity differential module.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
omit [DecidableEq H] in

Lean source · statement

theorem rightRegular_d₂₁_mem_relationSubmodule (x : H × H →₀ GroupRing H) :
    groupHomology.d₂₁ (rightRegularRep H) x ∈ relationSubmodule (MonoidHom.id H)

theorem

rightRegular_d₂₁_smul_single

L157 ↗

FoxDifferential.rightRegular_d₂₁_smul_single

Documentation

The scalar-multiplication formula for \(d_{21}\) holds on singleton generators.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
omit [DecidableEq H] in

Lean source · statement

theorem rightRegular_d₂₁_smul_single (r : GroupRing H) (g : H × H) (a : GroupRing H) :
    groupHomology.d₂₁ (rightRegularRep H) (r • Finsupp.single g a) =
      r • groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g a)

theorem

rightRegular_d₂₁_smul

L174 ↗

FoxDifferential.rightRegular_d₂₁_smul

Documentation

The right-regular \(d_{21}\) map is compatible with scalar multiplication.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
omit [DecidableEq H] in

Lean source · statement

theorem rightRegular_d₂₁_smul (r : GroupRing H) (x : H × H →₀ GroupRing H) :
    groupHomology.d₂₁ (rightRegularRep H) (r • x) =
      r • groupHomology.d₂₁ (rightRegularRep H) x

def

rightRegularBoundariesSubmodule

L188 ↗

FoxDifferential.rightRegularBoundariesSubmodule

Documentation

The degree-1 boundaries for the right-regular representation, regarded as a \(\mathbb{Z}[H]\)-submodule of the free pre-module.

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]

Lean source · full declaration

def rightRegularBoundariesSubmodule : Submodule (GroupRing H) (DifferentialPreModule H H) where
  carrier := groupHomology.boundaries₁ (rightRegularRep H)
  zero_mem' := by
    exact ⟨0, by simp only [map_zero]⟩
  add_mem' := by
    intro x y hx hy
    exact (groupHomology.boundaries₁ (rightRegularRep H)).add_mem hx hy
  smul_mem' := by
    intro r x hx
    rcases hx with ⟨y, rfl⟩
    exact ⟨r • y, rightRegular_d₂₁_smul (H := H) r y⟩

theorem

mem_rightRegularBoundariesSubmodule

L204 ↗

FoxDifferential.mem_rightRegularBoundariesSubmodule

Documentation

The displayed right-regular boundary lies in the right-regular boundary submodule.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem mem_rightRegularBoundariesSubmodule {x : DifferentialPreModule H H} :
    x ∈ rightRegularBoundariesSubmodule H ↔ x ∈ groupHomology.boundaries₁ (rightRegularRep H)

theorem

relationElement_mem_rightRegularBoundariesSubmodule

L210 ↗

FoxDifferential.relationElement_mem_rightRegularBoundariesSubmodule

Documentation

Each identity-Crowell relation already lies in the right-regular boundary submodule.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem relationElement_mem_rightRegularBoundariesSubmodule (g₁ g₂ : H) :
    relationElement (MonoidHom.id H) g₁ g₂ ∈ rightRegularBoundariesSubmodule H

theorem

relationSubmodule_le_rightRegularBoundariesSubmodule

L218 ↗

FoxDifferential.relationSubmodule_le_rightRegularBoundariesSubmodule

Documentation

The identity Crowell relation submodule is contained in the right-regular boundary submodule.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem relationSubmodule_le_rightRegularBoundariesSubmodule :
    relationSubmodule (MonoidHom.id H) ≤ rightRegularBoundariesSubmodule H

theorem

rightRegular_boundaries₁_le_relationSubmodule

L230 ↗

FoxDifferential.rightRegular_boundaries₁_le_relationSubmodule

Documentation

The degree-1 boundaries for the right-regular representation lie in the Crowell relation submodule.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegular_boundaries₁_le_relationSubmodule :
    groupHomology.boundaries₁ (rightRegularRep H) ≤
      (relationSubmodule (MonoidHom.id H)).restrictScalars ℤ

theorem

rightRegularBoundariesSubmodule_le_relationSubmodule

L239 ↗

FoxDifferential.rightRegularBoundariesSubmodule_le_relationSubmodule

Documentation

The right-regular boundary submodule is contained in the relation submodule.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegularBoundariesSubmodule_le_relationSubmodule :
    rightRegularBoundariesSubmodule H ≤ relationSubmodule (MonoidHom.id H)

theorem

relationSubmodule_eq_rightRegularBoundariesSubmodule

L246 ↗

FoxDifferential.relationSubmodule_eq_rightRegularBoundariesSubmodule

Documentation

The identity Crowell relations are exactly the right-regular degree-1 boundaries.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem relationSubmodule_eq_rightRegularBoundariesSubmodule :
    relationSubmodule (MonoidHom.id H) = rightRegularBoundariesSubmodule H

theorem

liftLinear_groupRingBoundary_id_single

L257 ↗

FoxDifferential.liftLinear_groupRingBoundary_id_single

Documentation

The lifted linear identity-boundary map has the stated value on a single group-ring generator.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem liftLinear_groupRingBoundary_id_single (g : H) (r : GroupRing H) :
    liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)) (Finsupp.single g r) =
      r * augmentationGenerator H g

theorem

liftLinear_groupRingBoundary_id_mem_augmentationIdeal

L266 ↗

FoxDifferential.liftLinear_groupRingBoundary_id_mem_augmentationIdeal

Documentation

The pre-boundary map for the identity case lands in the augmentation ideal.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem liftLinear_groupRingBoundary_id_mem_augmentationIdeal (x : DifferentialPreModule H H) :
    liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)) x ∈ augmentationIdeal H

theorem

augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id

L279 ↗

FoxDifferential.augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id

Documentation

The standard generator \(h-1\) of the augmentation ideal lies in the image of the identity pre-boundary map.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id (h : H) :
    augmentationGenerator H h ∈
      LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)))

theorem

augmentationIdeal_le_range_liftLinear_groupRingBoundary_id

L290 ↗

FoxDifferential.augmentationIdeal_le_range_liftLinear_groupRingBoundary_id

Documentation

The augmentation ideal is generated by the image of the identity pre-boundary map.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem augmentationIdeal_le_range_liftLinear_groupRingBoundary_id :
    (augmentationIdeal H : Submodule (GroupRing H) (GroupRing H)) ≤
      LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)))

theorem

liftLinear_groupRingBoundary_id_eq_d₁₀

L310 ↗

FoxDifferential.liftLinear_groupRingBoundary_id_eq_d₁₀

Documentation

For the identity homomorphism, the lifted group-ring boundary equals the degree-one differential for the right-regular representation.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem liftLinear_groupRingBoundary_id_eq_d₁₀ :
    (liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H))).restrictScalars ℤ =
      (groupHomology.d₁₀ (rightRegularRep H)).hom

theorem

liftLinear_groupRingBoundary_id_apply

L329 ↗

FoxDifferential.liftLinear_groupRingBoundary_id_apply

Documentation

The identity group-ring boundary lift is evaluated on canonical generators and then extended linearly.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem liftLinear_groupRingBoundary_id_apply (x : DifferentialPreModule H H) :
    liftLinear (H := H) (G := H) (A := GroupRing H)
        (groupRingBoundary (MonoidHom.id H)) x =
      groupHomology.d₁₀ (rightRegularRep H) x

theorem

rightRegular_d₁₀_mem_augmentationIdeal

L338 ↗

FoxDifferential.rightRegular_d₁₀_mem_augmentationIdeal

Documentation

The right-regular degree-0 differential lands in the augmentation ideal.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegular_d₁₀_mem_augmentationIdeal (x : DifferentialPreModule H H) :
    groupHomology.d₁₀ (rightRegularRep H) x ∈ augmentationIdeal H

theorem

rightRegular_d₁₀_range_eq_augmentationIdeal

L345 ↗

FoxDifferential.rightRegular_d₁₀_range_eq_augmentationIdeal

Documentation

The canonical augmentation ideal is the kernel of the ordinary group-ring augmentation map.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegular_d₁₀_range_eq_augmentationIdeal :
    LinearMap.range (groupHomology.d₁₀ (rightRegularRep H)).hom =
      (augmentationIdeal H).restrictScalars ℤ

abbrev

bottomTrivialRep

L362 ↗

FoxDifferential.bottomTrivialRep

Documentation

The trivial representation of the trivial subgroup of \(H\). Shapiro identifies its induced representation with the right-regular representation.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · statement

abbrev bottomTrivialRep : Rep ℤ (⊥ : Subgroup H)

def

indBottomTrivialUnderlyingEquiv

L366 ↗

FoxDifferential.indBottomTrivialUnderlyingEquiv

Documentation

The induced module from the trivial subgroup is just the group ring.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · statement

def indBottomTrivialUnderlyingEquiv :
    Representation.IndV (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ ≃ₗ[ℤ] GroupRing H

theorem

indBottomTrivialUnderlyingEquiv_mk

L382 ↗

FoxDifferential.indBottomTrivialUnderlyingEquiv_mk

Documentation

The bottom-trivial induced-module equivalence sends the induced representative with element \(h\) and coefficient \(n\) to the singleton group-ring element at \(h\) with coefficient \(n\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem indBottomTrivialUnderlyingEquiv_mk (h : H) (n : ℤ) :
    indBottomTrivialUnderlyingEquiv H
      (Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h n) =
        MonoidAlgebra.single h n

def

indBottomTrivialIsoRightRegular

L406 ↗

FoxDifferential.indBottomTrivialIsoRightRegular

Documentation

Shapiro's lemma identifies the induced trivial representation of the trivial subgroup with the right-regular representation.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · statement

def indBottomTrivialIsoRightRegular :
    Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H) ≅ rightRegularRep H

def

groupHomologyIsoOfRepIso

L432 ↗

FoxDifferential.groupHomologyIsoOfRepIso

Documentation

Group homology respects isomorphic representations.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · full declaration

def groupHomologyIsoOfRepIso {A B : Rep ℤ H} (e : A ≅ B) (n : ℕ) :
    groupHomology A n ≅ groupHomology B n where
  hom := groupHomology.map (MonoidHom.id H) e.hom n
  inv := groupHomology.map (MonoidHom.id H) e.inv n
  hom_inv_id := by
    have h := groupHomology.map_id_comp (φ := e.hom) (ψ := e.inv) (n := n)
    rw [e.hom_inv_id, groupHomology.map_id] at h
    simpa using h.symm
  inv_hom_id := by
    have h := groupHomology.map_id_comp (φ := e.inv) (ψ := e.hom) (n := n)
    rw [e.inv_hom_id, groupHomology.map_id] at h
    simpa using h.symm

def

rightRegularH1IsoBottom

L449 ↗

FoxDifferential.rightRegularH1IsoBottom

Documentation

The first homology of the right-regular representation is identified with the first homology of the trivial subgroup.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · statement

def rightRegularH1IsoBottom :
    groupHomology (rightRegularRep H) 1 ≅ groupHomology (bottomTrivialRep H) 1

theorem

rightRegular_H1_isZero

L456 ↗

FoxDifferential.rightRegular_H1_isZero

Documentation

The first homology of the right-regular representation vanishes.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegular_H1_isZero : Limits.IsZero (groupHomology (rightRegularRep H) 1)

theorem

rightRegular_cycles₁_eq_boundaries₁

L464 ↗

FoxDifferential.rightRegular_cycles₁_eq_boundaries₁

Documentation

In degree 1, right-regular cycles are exactly right-regular boundaries.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegular_cycles₁_eq_boundaries₁ :
    groupHomology.cycles₁ (rightRegularRep H) = groupHomology.boundaries₁ (rightRegularRep H)

theorem

mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero

L480 ↗

FoxDifferential.mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero

Documentation

For the right-regular representation, a 1-chain is a boundary exactly when its degree-0 differential vanishes.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · statement

theorem mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero
    {H : Type} [Group H] {x : DifferentialPreModule H H} :
    x ∈ rightRegularBoundariesSubmodule H ↔ groupHomology.d₁₀ (rightRegularRep H) x = 0

def

rightRegularBoundariesQuotientEquivIdentityDifferentialModule

L499 ↗

FoxDifferential.rightRegularBoundariesQuotientEquivIdentityDifferentialModule

Documentation

The quotient of the free pre-module by right-regular degree-1 boundaries is the identity Crowell differential module.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · statement

def rightRegularBoundariesQuotientEquivIdentityDifferentialModule :
    (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) ≃ₗ[GroupRing H]
      DifferentialModule (MonoidHom.id H)

theorem

rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk

L512 ↗

FoxDifferential.rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk

Documentation

The equivalence from the quotient by right-regular boundaries to the identity differential module sends a quotient class to the corresponding relation-submodule quotient class.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk
    (x : DifferentialPreModule H H) :
    rightRegularBoundariesQuotientEquivIdentityDifferentialModule H
      (Submodule.Quotient.mk x) =
        (relationSubmodule (MonoidHom.id H)).mkQ x

def

rightRegularBoundariesQuotientToAugmentationIdeal

L522 ↗

FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal

Documentation

The quotient by right-regular boundaries maps onto the augmentation ideal.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · statement

def rightRegularBoundariesQuotientToAugmentationIdeal :
    (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) →ₗ[GroupRing H]
      augmentationIdeal H

theorem

rightRegularBoundariesQuotientToAugmentationIdeal_mk_single

L541 ↗

FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal_mk_single

Documentation

The quotient map from right-regular boundaries to the augmentation ideal sends a single generator to the corresponding augmentation generator.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegularBoundariesQuotientToAugmentationIdeal_mk_single (h : H) :
    rightRegularBoundariesQuotientToAugmentationIdeal H
      (Submodule.Quotient.mk (Finsupp.single h 1)) =
        augmentationGeneratorSubtype (H := H) h

theorem

rightRegularBoundariesQuotientToAugmentationIdeal_surjective

L552 ↗

FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal_surjective

Documentation

The quotient by right-regular boundaries surjects onto the augmentation ideal.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegularBoundariesQuotientToAugmentationIdeal_surjective :
    Function.Surjective (rightRegularBoundariesQuotientToAugmentationIdeal H)

theorem

rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff

L561 ↗

FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff

Documentation

The quotient-to-augmentation map has trivial kernel.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · statement

theorem rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff
    {H : Type} [Group H]
    {q : DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)} :
    rightRegularBoundariesQuotientToAugmentationIdeal H q = 0 ↔ q = 0

theorem

rightRegularBoundariesQuotientToAugmentationIdeal_injective

L589 ↗

FoxDifferential.rightRegularBoundariesQuotientToAugmentationIdeal_injective

Documentation

The map from the quotient of right-regular boundaries to the ordinary augmentation ideal is injective.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem rightRegularBoundariesQuotientToAugmentationIdeal_injective :
    Function.Injective (rightRegularBoundariesQuotientToAugmentationIdeal H)

def

rightRegularBoundariesQuotientEquivAugmentationIdeal

L597 ↗

FoxDifferential.rightRegularBoundariesQuotientEquivAugmentationIdeal

Documentation

The right-regular boundary quotient is exactly the augmentation ideal.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in

Lean source · statement

def rightRegularBoundariesQuotientEquivAugmentationIdeal :
    (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) ≃ₗ[GroupRing H]
      augmentationIdeal H

theorem

identityDifferentialModuleEquivAugmentationIdeal_d

L610 ↗

FoxDifferential.identityDifferentialModuleEquivAugmentationIdeal_d

Documentation

Under the identity differential module equivalence, the universal differential \(d(h)\) corresponds to the augmentation generator \(h-1\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open CategoryTheory Limits Representation Rep TensorProduct
open scoped TensorProduct
variable (H : Type) [Group H] [DecidableEq H]
variable {H} in
omit [DecidableEq H] in

Lean source · statement

theorem identityDifferentialModuleEquivAugmentationIdeal_d (h : H) :
    identityDifferentialModuleEquivAugmentationIdeal (H := H)
        (universalDifferential (MonoidHom.id H) h) =
      augmentationGeneratorSubtype (H := H) h

Module documentation

Fox differential: discrete — kernel boundary — identity augmentation

Declarations