Documentation Verification Report

Basic

📁 Source: ClassFieldTheory/Cohomology/Subrep/Basic.lean

Statistics

Metric	Count
Definitions `Subrep`, `inclusion`, `instMin`, `instOrderTop`, `instPreorder`, `instSemilatticeInf`, `instSetLikeCarrierVModuleCat`, `isoOfEqTop`, `mkQ`, `quotient`, `subquotient`, `subrepOf`, `subrepOfIsoOfLE`, `subtype`, `toRep`, `toSubmodule`, `topIso`	17
Theorems `inclusion_comp_subtype`, `inclusion_comp_subtype_apply`, `inclusion_comp_subtype_assoc`, `instAddSubgroupClassCarrierVModuleCat`, `le_comap`, `mkQ_hom_hom_apply`, `subtype_hom_hom_apply`, `toSubmodule_inf`, `toSubmodule_injective`	9
Total	26

Subrep

Definitions

Name	Category	Theorems
`inclusion` 📖	CompOp	4 math math: `inclusion_comp_subtype`, `groupCohomology.map_inclusion_surjective_of_subsingleton_groupCohomology_subquotient`, `inclusion_comp_subtype_assoc`, `inclusion_comp_subtype_apply`
`instMin` 📖	CompOp	1 math math: `toSubmodule_inf`
`instOrderTop` 📖	CompOp	—
`instPreorder` 📖	CompOp	—
`instSemilatticeInf` 📖	CompOp	—
`instSetLikeCarrierVModuleCat` 📖	CompOp	1 math math: `instAddSubgroupClassCarrierVModuleCat`
`isoOfEqTop` 📖	CompOp	—
`mkQ` 📖	CompOp	1 math math: `mkQ_hom_hom_apply`
`quotient` 📖	CompOp	1 math math: `mkQ_hom_hom_apply`
`subquotient` 📖	CompOp	—
`subrepOf` 📖	CompOp	—
`subrepOfIsoOfLE` 📖	CompOp	—
`subtype` 📖	CompOp	5 math math: `inclusion_comp_subtype`, `inclusion_comp_subtype_assoc`, `subtype_hom_hom_apply`, `inclusion_comp_subtype_apply`, `toCochainsIso_symm_apply_coe`
`toRep` 📖	CompOp	8 math math: `inclusion_comp_subtype`, `toCochainsIso_apply_coe`, `groupCohomology.d_toCochainsIso_symm`, `groupCohomology.map_inclusion_surjective_of_subsingleton_groupCohomology_subquotient`, `inclusion_comp_subtype_assoc`, `subtype_hom_hom_apply`, `inclusion_comp_subtype_apply`, `toCochainsIso_symm_apply_coe`
`toSubmodule` 📖	CompOp	8 math math: `toSubmodule_inf`, `toRep_ext_iff`, `mkQ_hom_hom_apply`, `toCochainsIso_apply_coe`, `subtype_hom_hom_apply`, `toSubmodule_injective`, `IsFilterComplete.subrepToSubmodule`, `le_comap`
`topIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inclusion_comp_subtype` 📖	mathematical	`Subrep` `instPreorder`	`toRep` `inclusion` `subtype`	—	—
`inclusion_comp_subtype_apply` 📖	mathematical	`Subrep` `instPreorder`	`toRep` `subtype` `inclusion`	—	`inclusion_comp_subtype`
`inclusion_comp_subtype_assoc` 📖	mathematical	`Subrep` `instPreorder`	`toRep` `inclusion` `subtype`	—	`inclusion_comp_subtype`
`instAddSubgroupClassCarrierVModuleCat` 📖	mathematical	—	`Subrep` `instSetLikeCarrierVModuleCat`	—	—
`le_comap` 📖	mathematical	—	`toSubmodule`	—	—
`mkQ_hom_hom_apply` 📖	mathematical	—	`toSubmodule` `quotient` `mkQ`	—	—
`subtype_hom_hom_apply` 📖	mathematical	—	`toSubmodule` `toRep` `subtype`	—	—
`toSubmodule_inf` 📖	mathematical	—	`toSubmodule` `Subrep` `instMin`	—	—
`toSubmodule_injective` 📖	mathematical	—	`Subrep` `toSubmodule`	—	`le_comap`

(root)

Definitions

Name	Category	Theorems
`Subrep` 📖	CompData	3 math math: `Subrep.toSubmodule_inf`, `Subrep.instAddSubgroupClassCarrierVModuleCat`, `Subrep.toSubmodule_injective`

---

← Back to Index