Documentation Verification Report

Corestriction

📁 Source: ClassFieldTheory/Cohomology/Functors/Corestriction.lean

Statistics

Metric	Count
Definitions `cores₀_obj`, `coresNatTrans`, `cores_obj`, `cores₀`, `cores₁_obj`	5
Theorems `cores₀_obj_apply_coe`, `commSq_cores₁`, `commSq_cores₁_assoc`, `commSqₙ`, `cores_aux₁`, `cores_aux₂`, `cores_res`, `cores_res₀`, `cores_succ_naturality`, `cores₀_app`, `cores₁_naturality`, `groupCohomology_Sylow`, `injects_to_sylowCoh`, `map_H0Iso_hom_f_apply'`, `pTorsion_eq_sylowTorsion`, `torsion_of_finite_of_neZero`	16
Total	21

Rep

Definitions

Name	Category	Theorems
`cores₀_obj` 📖	CompOp	2 math math: `cores₀_obj_apply_coe`, `groupCohomology.cores₀_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cores₀_obj_apply_coe` 📖	mathematical	—	`res` `cores₀_obj`	—	—

groupCohomology

Definitions

Name	Category	Theorems
`coresNatTrans` 📖	CompOp	2 math math: `commSqₙ`, `cores_res`
`cores_obj` 📖	CompOp	1 math math: `cores_succ_naturality`
`cores₀` 📖	CompOp	4 math math: `cores_res₀`, `cores₀_app`, `commSq_cores₁`, `commSq_cores₁_assoc`
`cores₁_obj` 📖	CompOp	3 math math: `cores₁_naturality`, `commSq_cores₁`, `commSq_cores₁_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commSq_cores₁` 📖	mathematical	—	`Rep.dimensionShift.upSES` `Rep.res` `Rep.instAdditiveRes` `Rep.dimensionShift.shortExact_upSES_res` `cores₁_obj` `cores₀` `Rep.dimensionShift.shortExact_upSES`	—	`Rep.instAdditiveRes` `Rep.dimensionShift.shortExact_upSES_res` `Rep.dimensionShift.epi_δ_up_zero_res` `Rep.dimensionShift.shortExact_upSES`
`commSq_cores₁_assoc` 📖	mathematical	—	`Rep.dimensionShift.upSES` `Rep.res` `Rep.instAdditiveRes` `Rep.dimensionShift.shortExact_upSES_res` `cores₁_obj` `cores₀` `Rep.dimensionShift.shortExact_upSES`	—	`Rep.instAdditiveRes` `Rep.dimensionShift.shortExact_upSES_res` `Rep.dimensionShift.shortExact_upSES` `commSq_cores₁`
`commSqₙ` 📖	mathematical	—	`Rep.dimensionShift.up` `Rep.dimensionShift.upSES` `Rep.res` `rest` `coresNatTrans` `Rep.dimensionShift.shortExact_upSES`	—	`Rep.dimensionShift.shortExact_upSES` `CategoryTheory.comp_commSq` `Rep.instAdditiveRes` `Rep.dimensionShift.shortExact_upSES_res` `Rep.shortExact_res` `rest_δ_naturality` `commSq_cores₁`
`cores_aux₁` 📖	—	—	—	—	—
`cores_aux₂` 📖	—	—	—	—	`cores_aux₁`
`cores_res` 📖	mathematical	—	`Rep.res` `rest` `coresNatTrans`	—	`cores_res₀` `Rep.dimensionShift.shortExact_upSES` `Rep.dimensionShift.δ_up_zero_epi` `Rep.dimensionShift.δ_up_isIso` `commSqₙ`
`cores_res₀` 📖	mathematical	—	`Rep.res` `rest` `cores₀`	—	`map_H0Iso_hom_f_apply'`
`cores_succ_naturality` 📖	mathematical	—	`Rep.res` `cores_obj`	—	`cores₁_naturality` `Rep.instAdditiveRes` `Rep.dimensionShift.shortExact_upSES_res` `δ_naturality` `Rep.dimensionShift.shortExact_upSES`
`cores₀_app` 📖	mathematical	—	`Rep.res` `cores₀` `Rep.cores₀_obj`	—	—
`cores₁_naturality` 📖	mathematical	—	`Rep.res` `cores₁_obj`	—	`CategoryTheory.cubeLemma` `Rep.instAdditiveRes` `Rep.dimensionShift.shortExact_upSES_res` `Rep.dimensionShift.shortExact_upSES` `commSq_cores₁` `δ_naturality` `Rep.dimensionShift.epi_δ_up_zero_res`
`groupCohomology_Sylow` 📖	—	—	—	—	`pTorsion_eq_sylowTorsion` `injects_to_sylowCoh` `torsion_of_finite_of_neZero`
`injects_to_sylowCoh` 📖	mathematical	—	`Rep.res` `Module.IsTorsionBy.coprime_decompose` `torsion_of_finite_of_neZero`	—	`torsion_of_finite_of_neZero` `cores_res`
`map_H0Iso_hom_f_apply'` 📖	mathematical	—	`Rep.res`	—	—
`pTorsion_eq_sylowTorsion` 📖	—	—	—	—	`torsion_of_finite_of_neZero`
`torsion_of_finite_of_neZero` 📖	—	—	—	—	`cores_res` `Rep.isZero_of_trivialCohomology` `Rep.instTrivialCohomologyOfSubsingleton`

---

← Back to Index