Documentation Verification Report

TrivialCohomology

📁 Source: ClassFieldTheory/Cohomology/TrivialCohomology.lean

Statistics

Metric	Count
Definitions `TrivialCohomology`, `TrivialHomology`, `TrivialTateCohomology`, `zeroIso_ofTrivial`	4
Theorems `isZero`, `of_iso`, `res`, `res_subtype`, `isZero`, `of_injective`, `of_iso`, `res`, `res_subtype`, `isZero`, `of_cases`, `of_injective`, `of_iso`, `to_trivialCohomology`, `to_trivialHomology`, `instTrivialCohomologyOfSubsingleton`, `instTrivialHomologyOfSubsingleton`, `instTrivialTateCohomologyOfSubsingleton`, `isZero_of_injective`, `isZero_of_trivialCohomology`, `isZero_of_trivialHomology`, `isZero_of_trivialTateCohomology`, `trivialCohomology_iff_res`, `trivialHomology_iff_res`, `isIso_δ`	25
Total	29

Rep

Definitions

Name	Category	Theorems
`TrivialCohomology` 📖	CompData	20 math math: `trivialCohomology_ind₁'`, `dimensionShift.down_trivialCohomology`, `instTrivialCohomologyOfSubsingleton`, `groupCohomology.trivialCohomology_of_even_of_odd_of_solvable`, `trivialHomology_coind₁'`, `coind₁_quotientToInvariants_trivialCohomology`, `trivialCohomology_ind₁`, `TrivialCohomology.res_subtype`, `trivialCohomology_coind₁'`, `trivialCohomology_coind₁`, `trivialCohomology_iff_res`, `TrivialCohomology.res`, `trivialCohomology_coind₁AsPi`, `coind₁'_quotientToInvariants_trivialCohomology`, `leftRegular.trivialCohomology`, `dimensionShift.up_trivialCohomology`, `TrivialTateCohomology.to_trivialCohomology`, `TrivialCohomology.of_iso`, `groupCohomology.trivialCohomology_of_even_of_odd`, `split.trivialCohomology`
`TrivialHomology` 📖	CompData	13 math math: `TrivialHomology.of_iso`, `TrivialHomology.res`, `trivialHomology_of_trivialCohomology`, `leftRegular.trivialHomology`, `trivialHomology_ind₁'`, `trivialHomology_iff_res`, `trivialHomology_ind₁`, `trivialHomology_coind₁AsPi`, `trivialHomology_coind₁`, `instTrivialHomologyOfSubsingleton`, `TrivialHomology.res_subtype`, `trivialHomology_ind₁AsFinsupp`, `TrivialTateCohomology.to_trivialHomology`
`TrivialTateCohomology` 📖	CompData	10 math math: `TrivialTateCohomology.of_iso`, `trivialTateCohomology_coind₁'`, `leftRegular.trivialTateCohomology`, `tateCohomology_of_trivialCohomology`, `TrivialTateCohomology.of_cases`, `trivialTateCohomology_ind₁`, `instTrivialTateCohomologyOfSubsingleton`, `trivialTateCohomology_coind₁`, `trivialTateCohomology_ind₁'`, `trivialTateCohomology_coind₁AsPi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTrivialCohomologyOfSubsingleton` 📖	mathematical	—	`TrivialCohomology`	—	—
`instTrivialHomologyOfSubsingleton` 📖	mathematical	—	`TrivialHomology`	—	—
`instTrivialTateCohomologyOfSubsingleton` 📖	mathematical	—	`TrivialTateCohomology`	—	`TrivialTateCohomology.of_cases` `instTrivialCohomologyOfSubsingleton` `instTrivialHomologyOfSubsingleton`
`isZero_of_injective` 📖	mathematical	—	`res`	—	`TrivialCohomology.isZero`
`isZero_of_trivialCohomology` 📖	—	—	—	—	`isZero_of_injective`
`isZero_of_trivialHomology` 📖	—	—	—	—	`TrivialHomology.of_injective`
`isZero_of_trivialTateCohomology` 📖	mathematical	—	`groupCohomology.tateCohomology`	—	`TrivialTateCohomology.of_injective`
`trivialCohomology_iff_res` 📖	mathematical	—	`TrivialCohomology` `res`	—	`isZero_of_injective`
`trivialHomology_iff_res` 📖	mathematical	—	`TrivialHomology` `res`	—	`TrivialHomology.res`

Rep.TrivialCohomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isZero` 📖	mathematical	—	`Rep.res`	—	—
`of_iso` 📖	mathematical	—	`Rep.TrivialCohomology`	—	`isZero`
`res` 📖	mathematical	—	`Rep.TrivialCohomology` `Rep.res`	—	`Rep.isZero_of_injective`
`res_subtype` 📖	mathematical	—	`Rep.TrivialCohomology` `Rep.res`	—	`res`

Rep.TrivialHomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isZero` 📖	mathematical	—	`Rep.res`	—	—
`of_injective` 📖	mathematical	—	`Rep.res`	—	`isZero`
`of_iso` 📖	mathematical	—	`Rep.TrivialHomology`	—	`isZero`
`res` 📖	mathematical	—	`Rep.TrivialHomology` `Rep.res`	—	`of_injective`
`res_subtype` 📖	mathematical	—	`Rep.TrivialHomology` `Rep.res`	—	`res`

Rep.TrivialTateCohomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isZero` 📖	mathematical	—	`groupCohomology.tateCohomology` `Rep.res`	—	—
`of_cases` 📖	mathematical	`groupCohomology.tateCohomology` `Rep.res`	`Rep.TrivialTateCohomology`	—	`Rep.isZero_of_trivialCohomology` `Rep.TrivialCohomology.res_subtype` `Rep.isZero_of_trivialHomology` `Rep.TrivialHomology.res`
`of_injective` 📖	mathematical	—	`groupCohomology.tateCohomology` `Rep.res`	—	`isZero`
`of_iso` 📖	mathematical	—	`Rep.TrivialTateCohomology`	—	`isZero`
`to_trivialCohomology` 📖	mathematical	—	`Rep.TrivialCohomology`	—	`isZero`
`to_trivialHomology` 📖	mathematical	—	`Rep.TrivialHomology`	—	`isZero`

TateCohomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIso_δ` 📖	mathematical	—	`groupCohomology.tateCohomology` `groupCohomology.TateCohomology.δ`	—	`groupCohomology.TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1` `groupCohomology.TateCohomology.map_tateComplexFunctor_shortExact` `Rep.isZero_of_trivialTateCohomology`

TrivialTateCohomology

Definitions

Name	Category	Theorems
`zeroIso_ofTrivial` 📖	CompOp	—

---

← Back to Index