SerreApproximation

📁 Source: ClassFieldTheory/Cohomology/SerreApproximation.lean

Statistics

Metric	Count
Definitions `toCochains`, `toCochainsIso`, `toCochainsOrderHom`, `toCocycles`, `toCocyclesIso`, `toCocyclesOrderHom`, `cocyclesMapIso`, `kerDEquivCocycles`	8
Theorems `subrepToSubmodule`, `map_toCocycles_le_toCochains`, `toCochainsIso_apply_coe`, `toCochainsIso_symm_apply_coe`, `toCocycles_mem_toCocycles`, `toRep_ext`, `toRep_ext_iff`, `cochainsMap_d`, `cochainsMap_d_apply`, `cochainsMap_d_assoc`, `cocyclesMap_comp_iCocycles`, `cocyclesMap_comp_iCocycles_apply`, `cocyclesMap_comp_iCocycles_assoc`, `d_toCochainsIso_symm`, `exists_of_surjective`, `exists_of_π_eq_π`, `iCocycles_d`, `iCocycles_d'`, `iCocycles_d'_apply`, `iCocycles_d'_assoc`, `iCocycles_d_apply`, `iCocycles_d_assoc`, `iCocycles_injective`, `instIsFilterCompleteCarrierCocyclesNatSubmoduleToCocyclesOfVModuleCatSubrep`, `instIsFilterCompleteCarrierXNatModuleCatInhomogeneousCochainsSubmoduleToCochains`, `kerDEquivCocycles_apply`, `kerDEquivCocycles_symm_apply_coe`, `map_inclusion_surjective_of_subsingleton_groupCohomology_subquotient`, `subsingleton_of_subquotient`, `toCochains_le_comap_d`, `toCocycles_comp_π`, `toCocycles_comp_π_apply`, `toCocycles_comp_π_assoc`, `toCocycles_iCocycles`, `toCocycles_iCocycles_apply`, `toCocycles_iCocycles_assoc`, `toCycles_naturality`	37
Total	45

IsFilterComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subrepToSubmodule` 📖	mathematical	—	`IsFilterComplete` `Subrep.toSubmodule`	—	`Subrep.instAddSubgroupClassCarrierVModuleCat` `forget`

Subrep

Definitions

Name	Category	Theorems
`toCochains` 📖	CompOp	6 math math: `map_toCocycles_le_toCochains`, `toCochainsIso_apply_coe`, `groupCohomology.toCochains_le_comap_d`, `groupCohomology.d_toCochainsIso_symm`, `groupCohomology.instIsFilterCompleteCarrierXNatModuleCatInhomogeneousCochainsSubmoduleToCochains`, `toCochainsIso_symm_apply_coe`
`toCochainsIso` 📖	CompOp	3 math math: `toCochainsIso_apply_coe`, `groupCohomology.d_toCochainsIso_symm`, `toCochainsIso_symm_apply_coe`
`toCochainsOrderHom` 📖	CompOp	—
`toCocycles` 📖	CompOp	3 math math: `groupCohomology.instIsFilterCompleteCarrierCocyclesNatSubmoduleToCocyclesOfVModuleCatSubrep`, `map_toCocycles_le_toCochains`, `toCocycles_mem_toCocycles`
`toCocyclesIso` 📖	CompOp	—
`toCocyclesOrderHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_toCocycles_le_toCochains` 📖	mathematical	—	`toCocycles` `toCochains`	—	—
`toCochainsIso_apply_coe` 📖	mathematical	—	`toSubmodule` `toCochains` `toRep` `toCochainsIso`	—	—
`toCochainsIso_symm_apply_coe` 📖	mathematical	—	`toCochains` `toRep` `toCochainsIso` `subtype`	—	—
`toCocycles_mem_toCocycles` 📖	mathematical	`toCochains`	`toCocycles`	—	`ModuleCat.Hom.hom.eq_1` `groupCohomology.toCocycles_iCocycles_apply` `le_comap`
`toRep_ext` 📖	—	`toSubmodule`	—	—	—
`toRep_ext_iff` 📖	mathematical	—	`toSubmodule`	—	`toRep_ext`

groupCohomology

Definitions

Name	Category	Theorems
`cocyclesMapIso` 📖	CompOp	—
`kerDEquivCocycles` 📖	CompOp	2 math math: `kerDEquivCocycles_apply`, `kerDEquivCocycles_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cochainsMap_d` 📖	—	—	—	—	—
`cochainsMap_d_apply` 📖	—	—	—	—	`cochainsMap_d`
`cochainsMap_d_assoc` 📖	—	—	—	—	`cochainsMap_d`
`cocyclesMap_comp_iCocycles` 📖	—	—	—	—	—
`cocyclesMap_comp_iCocycles_apply` 📖	—	—	—	—	`cocyclesMap_comp_iCocycles`
`cocyclesMap_comp_iCocycles_assoc` 📖	—	—	—	—	`cocyclesMap_comp_iCocycles`
`d_toCochainsIso_symm` 📖	mathematical	—	`Subrep.toCochains` `Subrep.toRep` `Subrep.toCochainsIso`	—	`Subrep.le_comap`
`exists_of_surjective` 📖	—	—	—	—	`exists_of_π_eq_π`
`exists_of_π_eq_π` 📖	—	—	—	—	—
`iCocycles_d` 📖	—	—	—	—	—
`iCocycles_d'` 📖	—	—	—	—	`iCocycles_d`
`iCocycles_d'_apply` 📖	—	—	—	—	`iCocycles_d'`
`iCocycles_d'_assoc` 📖	—	—	—	—	`iCocycles_d'`
`iCocycles_d_apply` 📖	—	—	—	—	`iCocycles_d`
`iCocycles_d_assoc` 📖	—	—	—	—	`iCocycles_d`
`iCocycles_injective` 📖	—	—	—	—	—
`instIsFilterCompleteCarrierCocyclesNatSubmoduleToCocyclesOfVModuleCatSubrep` 📖	mathematical	—	`IsFilterComplete` `Subrep.toCocycles`	—	`Subrep.instAddSubgroupClassCarrierVModuleCat` `IsFilterComplete.ker` `instIsFilterCompleteCarrierXNatModuleCatInhomogeneousCochainsSubmoduleToCochains` `IsFilterComplete.toIsFilterHausdorff` `toCochains_le_comap_d` `IsFilterComplete.of_iso`
`instIsFilterCompleteCarrierXNatModuleCatInhomogeneousCochainsSubmoduleToCochains` 📖	mathematical	—	`IsFilterComplete` `Subrep.toCochains`	—	`Subrep.instAddSubgroupClassCarrierVModuleCat` `IsFilterComplete.piLeft` `IsFilterComplete.subrepToSubmodule`
`kerDEquivCocycles_apply` 📖	mathematical	—	`kerDEquivCocycles`	—	—
`kerDEquivCocycles_symm_apply_coe` 📖	mathematical	—	`kerDEquivCocycles`	—	—
`map_inclusion_surjective_of_subsingleton_groupCohomology_subquotient` 📖	mathematical	`Subrep` `Subrep.instPreorder`	`Subrep.toRep` `Subrep.inclusion`	—	`Subrep.shortExact_of_le`
`subsingleton_of_subquotient` 📖	—	`Subrep` `Subrep.instPreorder` `Subrep.instOrderTop` `Subrep.subquotient`	—	—	`Subrep.instAddSubgroupClassCarrierVModuleCat` `map_inclusion_surjective_of_subsingleton_groupCohomology_subquotient` `instIsFilterCompleteCarrierXNatModuleCatInhomogeneousCochainsSubmoduleToCochains` `instIsFilterCompleteCarrierCocyclesNatSubmoduleToCocyclesOfVModuleCatSubrep` `exists_of_surjective` `Subrep.toCocycles_mem_toCocycles` `IsFilterComplete.map_sum` `Filtration.ext` `IsFilterComplete.toIsFilterHausdorff` `sub_mem_trans` `IsFilterComplete.sum_sub_mem` `sub_mem_symm` `toCycles_naturality` `toCocycles_comp_π_apply`
`toCochains_le_comap_d` 📖	mathematical	—	`Subrep.toCochains`	—	`d_toCochainsIso_symm`
`toCocycles_comp_π` 📖	—	—	—	—	—
`toCocycles_comp_π_apply` 📖	—	—	—	—	`toCocycles_comp_π`
`toCocycles_comp_π_assoc` 📖	—	—	—	—	`toCocycles_comp_π`
`toCocycles_iCocycles` 📖	—	—	—	—	—
`toCocycles_iCocycles_apply` 📖	—	—	—	—	`toCocycles_iCocycles`
`toCocycles_iCocycles_assoc` 📖	—	—	—	—	`toCocycles_iCocycles`
`toCycles_naturality` 📖	—	—	—	—	`cocyclesMap_comp_iCocycles` `toCocycles_iCocycles_assoc` `toCocycles_iCocycles` `cochainsMap_d`

---

← Back to Index