Documentation Verification Report

H1

📁 Source: Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean

Statistics

Metric	Count
Definitions `H1`, `OneCochain`, `ev`, `instGroup`, `instInv`, `instMul`, `instOne`, `OneCocycle`, `IsCohomologous`, `class`, `instOne`, `toOneCochain`, `OneCohomologyRelation`, `ZeroCochain`, `instGroupZeroCochain`, `instOneH1`, `H1`, `H1`	18
Theorems `inv_apply`, `mul_apply`, `one_apply`, `ev_precomp`, `ext`, `ext_iff`, `inv_ev`, `mul_ev`, `one_ev`, `class_eq`, `class_eq_iff`, `equivalence_isCohomologous`, `ev_refl`, `ev_symm`, `ev_trans`, `one_toOneCochain`, `refl`, `trans`	18
Total	36

CategoryTheory.PresheafOfGroups

Definitions

Name	Category	Theorems
`H1` 📖	CompOp	—
`OneCochain` 📖	CompData	4 math math: `OneCochain.one_ev`, `OneCocycle.one_toOneCochain`, `OneCochain.mul_ev`, `OneCochain.inv_ev`
`OneCocycle` 📖	CompData	2 math math: `OneCocycle.one_toOneCochain`, `OneCocycle.equivalence_isCohomologous`
`OneCohomologyRelation` 📖	MathDef	1 math math: `OneCohomologyRelation.refl`
`ZeroCochain` 📖	CompOp	6 math math: `Cochain₀.inv_apply`, `Cochain₀.one_apply`, `OneCohomologyRelation.refl`, `OneCohomologyRelation.trans`, `OneCohomologyRelation.symm`, `Cochain₀.mul_apply`
`instGroupZeroCochain` 📖	CompOp	6 math math: `Cochain₀.inv_apply`, `Cochain₀.one_apply`, `OneCohomologyRelation.refl`, `OneCohomologyRelation.trans`, `OneCohomologyRelation.symm`, `Cochain₀.mul_apply`
`instOneH1` 📖	CompOp	—

CategoryTheory.PresheafOfGroups.Cochain₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_apply` 📖	mathematical	—	`CategoryTheory.PresheafOfGroups.ZeroCochain` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `CategoryTheory.PresheafOfGroups.instGroupZeroCochain` `GrpCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `GrpCat.str`	—	—
`mul_apply` 📖	mathematical	—	`CategoryTheory.PresheafOfGroups.ZeroCochain` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.PresheafOfGroups.instGroupZeroCochain` `GrpCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `GrpCat.str`	—	—
`one_apply` 📖	mathematical	—	`CategoryTheory.PresheafOfGroups.ZeroCochain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `CategoryTheory.PresheafOfGroups.instGroupZeroCochain` `GrpCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `GrpCat.str`	—	—

CategoryTheory.PresheafOfGroups.OneCochain

Definitions

Name	Category	Theorems
`ev` 📖	CompOp	8 math math: `one_ev`, `CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans`, `CategoryTheory.PresheafOfGroups.OneCocycle.ev_symm`, `mul_ev`, `ev_precomp`, `ext_iff`, `CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl`, `inv_ev`
`instGroup` 📖	CompOp	—
`instInv` 📖	CompOp	1 math math: `inv_ev`
`instMul` 📖	CompOp	1 math math: `mul_ev`
`instOne` 📖	CompOp	2 math math: `one_ev`, `CategoryTheory.PresheafOfGroups.OneCocycle.one_toOneCochain`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ev_precomp` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `GrpCat.carrier` `CategoryTheory.ConcreteCategory.hom` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `MonoidHom.instFunLike` `GrpCat.instConcreteCategoryMonoidHomCarrier` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `ev` `CategoryTheory.CategoryStruct.comp`	—	—
`ext` 📖	—	`ev`	—	—	—
`ext_iff` 📖	mathematical	—	`ev`	—	`ext`
`inv_ev` 📖	mathematical	—	`ev` `CategoryTheory.PresheafOfGroups.OneCochain` `instInv` `GrpCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `GrpCat.str`	—	—
`mul_ev` 📖	mathematical	—	`ev` `CategoryTheory.PresheafOfGroups.OneCochain` `instMul` `GrpCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str`	—	—
`one_ev` 📖	mathematical	—	`ev` `CategoryTheory.PresheafOfGroups.OneCochain` `instOne` `GrpCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `GrpCat.str`	—	—

CategoryTheory.PresheafOfGroups.OneCocycle

Definitions

Name	Category	Theorems
`IsCohomologous` 📖	MathDef	2 math math: `class_eq_iff`, `equivalence_isCohomologous`
`class` 📖	CompOp	2 math math: `IsCohomologous.class_eq`, `class_eq_iff`
`instOne` 📖	CompOp	1 math math: `one_toOneCochain`
`toOneCochain` 📖	CompOp	4 math math: `ev_trans`, `one_toOneCochain`, `ev_symm`, `ev_refl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`class_eq_iff` 📖	mathematical	—	`class` `IsCohomologous`	—	`Equivalence.quot_mk_eq_iff` `equivalence_isCohomologous`
`equivalence_isCohomologous` 📖	mathematical	—	`CategoryTheory.PresheafOfGroups.OneCocycle` `IsCohomologous`	—	`CategoryTheory.PresheafOfGroups.OneCohomologyRelation.refl` `CategoryTheory.PresheafOfGroups.OneCohomologyRelation.symm` `CategoryTheory.PresheafOfGroups.OneCohomologyRelation.trans`
`ev_refl` 📖	mathematical	—	`CategoryTheory.PresheafOfGroups.OneCochain.ev` `toOneCochain` `GrpCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `GrpCat.str`	—	`LeftCancelSemigroup.toIsLeftCancelMul` `ev_trans`
`ev_symm` 📖	mathematical	—	`CategoryTheory.PresheafOfGroups.OneCochain.ev` `toOneCochain` `GrpCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `GrpCat.str`	—	`RightCancelSemigroup.toIsRightCancelMul` `ev_trans` `ev_refl` `inv_mul_cancel`
`ev_trans` 📖	mathematical	—	`GrpCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `GrpCat` `GrpCat.instCategory` `Opposite.op` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `GrpCat.str` `CategoryTheory.PresheafOfGroups.OneCochain.ev` `toOneCochain`	—	—
`one_toOneCochain` 📖	mathematical	—	`toOneCochain` `CategoryTheory.PresheafOfGroups.OneCocycle` `instOne` `CategoryTheory.PresheafOfGroups.OneCochain` `CategoryTheory.PresheafOfGroups.OneCochain.instOne`	—	—

CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`class_eq` 📖	mathematical	`CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous`	`CategoryTheory.PresheafOfGroups.OneCocycle.class`	—	—

CategoryTheory.PresheafOfGroups.OneCohomologyRelation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`CategoryTheory.PresheafOfGroups.OneCohomologyRelation` `CategoryTheory.PresheafOfGroups.ZeroCochain` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `CategoryTheory.PresheafOfGroups.instGroupZeroCochain`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `one_mul` `mul_one`
`trans` 📖	mathematical	`CategoryTheory.PresheafOfGroups.OneCohomologyRelation`	`CategoryTheory.PresheafOfGroups.ZeroCochain` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.PresheafOfGroups.instGroupZeroCochain`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `mul_assoc`

groupCohomology

Definitions

Name	Category	Theorems
`H1` 📖	CompOp	16 math math: `H1π_comp_map_assoc`, `π_comp_H1Iso_hom_assoc`, `H1IsoOfIsTrivial_inv_apply`, `H1IsoOfIsTrivial_H1π_apply_apply`, `δ₁_apply`, `π_comp_H1Iso_hom`, `instEpiModuleCatH1π`, `H1π_eq_zero_iff`, `H1π_comp_H1IsoOfIsTrivial_hom_apply`, `H1π_comp_map_apply`, `δ₀_apply`, `π_comp_H1Iso_hom_apply`, `H1π_comp_H1IsoOfIsTrivial_hom`, `H1π_comp_map`, `H1π_comp_H1IsoOfIsTrivial_hom_assoc`, `H1π_eq_iff`

groupHomology

Definitions

Name	Category	Theorems
`H1` 📖	CompOp	26 math math: `H1CoresCoinf_X₃`, `δ₀_apply`, `π_comp_H1Iso_inv`, `H1CoresCoinfOfTrivial_X₁`, `H1CoresCoinf_X₁`, `H1CoresCoinfOfTrivial_X₂`, `H1CoresCoinf_X₂`, `H1π_comp_map_apply`, `H1AddEquivOfIsTrivial_single`, `π_comp_H1Iso_hom_apply`, `H1AddEquivOfIsTrivial_symm_apply`, `H1ToTensorOfIsTrivial_H1π_single`, `H1π_eq_zero_iff`, `π_comp_H1Iso_hom_assoc`, `H1π_comp_map_assoc`, `instEpiModuleCatH1π`, `H1AddEquivOfIsTrivial_apply`, `H1π_comp_map`, `π_comp_H1Iso_hom`, `mkH1OfIsTrivial_apply`, `π_comp_H1Iso_inv_apply`, `H1CoresCoinfOfTrivial_X₃`, `H1AddEquivOfIsTrivial_symm_tmul`, `π_comp_H1Iso_inv_assoc`, `δ₁_apply`, `H1π_eq_iff`

---

← Back to Index