Finite

📁 Source: ClassFieldTheory/Cohomology/IndCoind/Finite.lean

Statistics

Metric	Count
Definitions `coind₁`, `coind₁'`, `coind₁'_obj_iso_coind₁`, `coind₁'_ι`, `coind₁AsPi`, `coind₁AsPiIso`, `coind₁_quotientToInvariants_iso`, `coind₁_quotientToInvariants_iso_aux1`, `coind₁_quotientToInvariants_iso_aux2`, `ind₁`, `ind₁'`, `ind₁'_iso_coind₁'`, `ind₁'_obj_iso_ind₁`, `ind₁'_π`, `ind₁AsFinsupp`, `ind₁AsFinsuppIso`, `ind₁_obj_iso_coind₁_obj`, `instDecidableRelR_classFieldTheory`, `iso_ind₁`, `Ind₁V`, `mk`, `coind₁`, `coind₁'`, `coind₁'_lequiv_coind₁`, `coind₁'_ι`, `coind₁AsPi`, `coind₁V`, `ind₁`, `ind₁'`, `ind₁'_invlmap`, `ind₁'_invlmap_aux`, `ind₁'_lequiv`, `ind₁'_lequiv_coind₁'`, `ind₁'_lmap`, `ind₁'_map`, `ind₁'_π`, `ind₁AsFinsupp`, `instCoeForallSubtypeMemSubmoduleCoind₁V`, `instFunLikeSubtypeForallMemSubmoduleCoind₁V`	39
Theorems `coind₁'_obj`, `coind₁'_obj_iso_coind₁_hom_hom`, `coind₁'_obj_iso_coind₁_inv_hom`, `coind₁'_ι_app_hom`, `ind₁'_iso_coind₁'_app_apply`, `ind₁'_obj`, `ind₁'_obj_ρ`, `ind₁'_obj_ρ_apply`, `ind₁'_π_app_hom`, `ind₁_obj_ρ`, `instEpiAppInd₁'_π`, `instMonoAppCoind₁'_ι`, `coind₁'_apply_apply`, `coind₁'_apply₃`, `coind₁'_lequiv_coind₁_apply_coe`, `coind₁'_lequiv_coind₁_comm`, `coind₁'_lequiv_coind₁_symm_apply`, `coind₁'_ι_app_injective`, `coind₁'_ι_apply`, `coind₁'_ι_comm`, `coind₁AsPi_apply`, `coind₁AsPi_single`, `coind₁_apply₃`, `ind₁'_apply`, `ind₁'_apply₂`, `ind₁'_comp_lsingle`, `ind₁'_lequiv_apply`, `ind₁'_lequiv_coind₁'_apply`, `ind₁'_lequiv_coind₁'_comm`, `ind₁'_lequiv_coind₁'_comm'`, `ind₁'_lequiv_comm`, `ind₁'_lequiv_comp_lsingle`, `ind₁'_lequiv_symm_apply`, `ind₁'_lmap_apply`, `ind₁'_map_comm`, `ind₁'_π_apply`, `ind₁'_π_comm`, `ind₁'_π_comp_lsingle`, `ind₁AsFinsupp_apply`, `ind₁AsFinsupp_single`, `ind₁_apply`	41
Total	80

Rep

Definitions

Name	Category	Theorems
`coind₁` 📖	CompOp	6 math math: `coind₁_quotientToInvariants_trivialCohomology`, `trivialCohomology_coind₁`, `trivialHomology_coind₁`, `coind₁'_obj_iso_coind₁_hom_hom`, `trivialTateCohomology_coind₁`, `coind₁'_obj_iso_coind₁_inv_hom`
`coind₁'` 📖	CompOp	25 math math: `ind₁'_iso_coind₁'_app_apply`, `periodSeq₁_f`, `trivialTateCohomology_coind₁'`, `periodSeq₁_X₂`, `dimensionShift.upSES_X₂`, `dimensionShift.upSES_f`, `instMonoAppCoind₁'_ι`, `map₁_comp_ind₁'_iso_coind₁'`, `dimensionShift.up_map`, `trivialHomology_coind₁'`, `coind_ι_gg_map₁_app`, `coind₁'_ι_app_hom`, `trivialCohomology_coind₁'`, `dimensionShift.up_obj`, `periodSeq₂_f`, `periodSeq₂Functor_map`, `coind₁'_quotientToInvariants_trivialCohomology`, `periodSeq₁Functor_map`, `coind₁'_obj_iso_coind₁_hom_hom`, `periodSeq₁_g`, `coind_ι_gg_map₁`, `periodSeq₂_X₁`, `coind₁'_obj_iso_coind₁_inv_hom`, `dimensionShift.upShortComplex_map_τ₂`, `coind₁'_obj`
`coind₁'_obj_iso_coind₁` 📖	CompOp	2 math math: `coind₁'_obj_iso_coind₁_hom_hom`, `coind₁'_obj_iso_coind₁_inv_hom`
`coind₁'_ι` 📖	CompOp	8 math math: `periodSeq₁_f`, `dimensionShift.upSES_f`, `instMonoAppCoind₁'_ι`, `dimensionShift.up_map`, `coind_ι_gg_map₁_app`, `coind₁'_ι_app_hom`, `dimensionShift.up_obj`, `coind_ι_gg_map₁`
`coind₁AsPi` 📖	CompOp	3 math math: `trivialHomology_coind₁AsPi`, `trivialCohomology_coind₁AsPi`, `trivialTateCohomology_coind₁AsPi`
`coind₁AsPiIso` 📖	CompOp	—
`coind₁_quotientToInvariants_iso` 📖	CompOp	—
`coind₁_quotientToInvariants_iso_aux1` 📖	CompOp	—
`coind₁_quotientToInvariants_iso_aux2` 📖	CompOp	—
`ind₁` 📖	CompOp	4 math math: `trivialCohomology_ind₁`, `ind₁_obj_ρ`, `trivialHomology_ind₁`, `trivialTateCohomology_ind₁`
`ind₁'` 📖	CompOp	24 math math: `trivialCohomology_ind₁'`, `ind₁'_iso_coind₁'_app_apply`, `ind₁'_π_app_hom`, `dimensionShift.down_map`, `dimensionShift.downSES_X₂`, `map₁_comp_ind₁'_iso_coind₁'`, `map₂_gg_ind₁'_π`, `instEpiAppInd₁'_π`, `trivialHomology_ind₁'`, `ind₁'_obj_ρ_apply`, `dimensionShift.down_obj`, `ind₁'_obj`, `periodSeq₂_f`, `ind₁'_obj_ρ`, `periodSeq₂Functor_map`, `dimensionShift.downShortComplex_map_τ₂`, `periodSeq₁_X₃`, `periodSeq₁Functor_map`, `periodSeq₁_g`, `map₂_app_gg_ind₁'_π_app`, `periodSeq₂_g`, `dimensionShift.downSES_g`, `trivialTateCohomology_ind₁'`, `periodSeq₂_X₂`
`ind₁'_iso_coind₁'` 📖	CompOp	4 math math: `ind₁'_iso_coind₁'_app_apply`, `map₁_comp_ind₁'_iso_coind₁'`, `periodSeq₂_f`, `periodSeq₁_g`
`ind₁'_obj_iso_ind₁` 📖	CompOp	—
`ind₁'_π` 📖	CompOp	8 math math: `ind₁'_π_app_hom`, `dimensionShift.down_map`, `map₂_gg_ind₁'_π`, `instEpiAppInd₁'_π`, `dimensionShift.down_obj`, `map₂_app_gg_ind₁'_π_app`, `periodSeq₂_g`, `dimensionShift.downSES_g`
`ind₁AsFinsupp` 📖	CompOp	1 math math: `trivialHomology_ind₁AsFinsupp`
`ind₁AsFinsuppIso` 📖	CompOp	—
`ind₁_obj_iso_coind₁_obj` 📖	CompOp	—
`instDecidableRelR_classFieldTheory` 📖	CompOp	—
`iso_ind₁` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coind₁'_obj` 📖	mathematical	—	`coind₁'` `Representation.coind₁'`	—	—
`coind₁'_obj_iso_coind₁_hom_hom` 📖	mathematical	—	`coind₁'` `coind₁` `coind₁'_obj_iso_coind₁` `Representation.coind₁V` `Representation.coind₁'_lequiv_coind₁`	—	—
`coind₁'_obj_iso_coind₁_inv_hom` 📖	mathematical	—	`coind₁` `coind₁'` `coind₁'_obj_iso_coind₁` `Representation.coind₁V` `Representation.coind₁'_lequiv_coind₁`	—	—
`coind₁'_ι_app_hom` 📖	mathematical	—	`coind₁'` `coind₁'_ι` `Representation.coind₁'_ι`	—	—
`ind₁'_iso_coind₁'_app_apply` 📖	mathematical	—	`ind₁'` `coind₁'` `ind₁'_iso_coind₁'`	—	—
`ind₁'_obj` 📖	mathematical	—	`ind₁'` `Representation.ind₁'`	—	—
`ind₁'_obj_ρ` 📖	mathematical	—	`ind₁'` `Representation.ind₁'`	—	—
`ind₁'_obj_ρ_apply` 📖	mathematical	—	`ind₁'`	—	—
`ind₁'_π_app_hom` 📖	mathematical	—	`ind₁'` `ind₁'_π` `Representation.ind₁'_π`	—	—
`ind₁_obj_ρ` 📖	mathematical	—	`ind₁` `Representation.ind₁`	—	—
`instEpiAppInd₁'_π` 📖	mathematical	—	`ind₁'` `ind₁'_π`	—	—
`instMonoAppCoind₁'_ι` 📖	mathematical	—	`coind₁'` `coind₁'_ι`	—	—

Representation

Definitions

Name	Category	Theorems
`Ind₁V` 📖	CompOp	5 math math: `ind₁'_lequiv_apply`, `ind₁'_lequiv_symm_apply`, `ind₁'_lequiv_comp_lsingle`, `ind₁'_lmap_apply`, `ind₁'_lequiv_comm`
`coind₁` 📖	CompOp	2 math math: `coind₁_apply₃`, `coind₁'_lequiv_coind₁_comm`
`coind₁'` 📖	CompOp	8 math math: `coind₁'_apply₃`, `ind₁'_lequiv_coind₁'_comm`, `coind₁'_ι_comm`, `map₁_comm`, `ind₁'_lequiv_coind₁'_comm'`, `coind₁'_apply_apply`, `coind₁'_lequiv_coind₁_comm`, `Rep.coind₁'_obj`
`coind₁'_lequiv_coind₁` 📖	CompOp	5 math math: `coind₁'_lequiv_coind₁_symm_apply`, `Rep.coind₁'_obj_iso_coind₁_hom_hom`, `coind₁'_lequiv_coind₁_apply_coe`, `Rep.coind₁'_obj_iso_coind₁_inv_hom`, `coind₁'_lequiv_coind₁_comm`
`coind₁'_ι` 📖	CompOp	6 math math: `map₁_ker`, `coind₁'_ι_app_injective`, `Rep.coind₁'_ι_app_hom`, `coind₁'_ι_apply`, `map₁_comp_coind_ι`, `coind₁'_ι_comm`
`coind₁AsPi` 📖	CompOp	2 math math: `coind₁AsPi_apply`, `coind₁AsPi_single`
`coind₁V` 📖	CompOp	6 math math: `coind₁_apply₃`, `coind₁'_lequiv_coind₁_symm_apply`, `Rep.coind₁'_obj_iso_coind₁_hom_hom`, `coind₁'_lequiv_coind₁_apply_coe`, `Rep.coind₁'_obj_iso_coind₁_inv_hom`, `coind₁'_lequiv_coind₁_comm`
`ind₁` 📖	CompOp	3 math math: `Rep.ind₁_obj_ρ`, `ind₁_apply`, `ind₁'_lequiv_comm`
`ind₁'` 📖	CompOp	13 math math: `map₂_comm`, `ind₁'_apply`, `Rep.aug.leftRegularToInd₁'_comm`, `ind₁'_comp_lsingle`, `ind₁'_lequiv_coind₁'_comm`, `Rep.ind₁'_obj`, `Rep.ind₁'_obj_ρ`, `Rep.aug.leftRegularToInd₁'_comm'`, `ind₁'_apply₂`, `ind₁'_lequiv_comm`, `ind₁'_map_comm`, `ind₁'_lequiv_coind₁'_comm'`, `ind₁'_π_comm`
`ind₁'_invlmap` 📖	CompOp	1 math math: `ind₁'_lequiv_symm_apply`
`ind₁'_invlmap_aux` 📖	CompOp	—
`ind₁'_lequiv` 📖	CompOp	4 math math: `ind₁'_lequiv_apply`, `ind₁'_lequiv_symm_apply`, `ind₁'_lequiv_comp_lsingle`, `ind₁'_lequiv_comm`
`ind₁'_lequiv_coind₁'` 📖	CompOp	3 math math: `ind₁'_lequiv_coind₁'_comm`, `ind₁'_lequiv_coind₁'_apply`, `ind₁'_lequiv_coind₁'_comm'`
`ind₁'_lmap` 📖	CompOp	1 math math: `ind₁'_lmap_apply`
`ind₁'_map` 📖	CompOp	1 math math: `ind₁'_map_comm`
`ind₁'_π` 📖	CompOp	6 math math: `Rep.ind₁'_π_app_hom`, `ind₁'_π_comp_map₂`, `map₂_range`, `ind₁'_π_comp_lsingle`, `ind₁'_π_apply`, `ind₁'_π_comm`
`ind₁AsFinsupp` 📖	CompOp	2 math math: `ind₁AsFinsupp_apply`, `ind₁AsFinsupp_single`
`instCoeForallSubtypeMemSubmoduleCoind₁V` 📖	CompOp	—
`instFunLikeSubtypeForallMemSubmoduleCoind₁V` 📖	CompOp	2 math math: `coind₁_apply₃`, `coind₁'_lequiv_coind₁_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coind₁'_apply_apply` 📖	mathematical	—	`coind₁'`	—	—
`coind₁'_apply₃` 📖	mathematical	—	`coind₁'`	—	—
`coind₁'_lequiv_coind₁_apply_coe` 📖	mathematical	—	`coind₁V` `coind₁'_lequiv_coind₁`	—	—
`coind₁'_lequiv_coind₁_comm` 📖	mathematical	—	`coind₁V` `coind₁'_lequiv_coind₁` `coind₁'` `coind₁`	—	—
`coind₁'_lequiv_coind₁_symm_apply` 📖	mathematical	—	`coind₁V` `coind₁'_lequiv_coind₁` `instFunLikeSubtypeForallMemSubmoduleCoind₁V`	—	—
`coind₁'_ι_app_injective` 📖	mathematical	—	`coind₁'_ι`	—	—
`coind₁'_ι_apply` 📖	mathematical	—	`coind₁'_ι`	—	—
`coind₁'_ι_comm` 📖	mathematical	—	`coind₁'` `coind₁'_ι`	—	—
`coind₁AsPi_apply` 📖	mathematical	—	`coind₁AsPi`	—	—
`coind₁AsPi_single` 📖	mathematical	—	`coind₁AsPi`	—	—
`coind₁_apply₃` 📖	mathematical	—	`instFunLikeSubtypeForallMemSubmoduleCoind₁V` `coind₁` `coind₁V`	—	—
`ind₁'_apply` 📖	mathematical	—	`ind₁'`	—	—
`ind₁'_apply₂` 📖	mathematical	—	`ind₁'`	—	—
`ind₁'_comp_lsingle` 📖	mathematical	—	`ind₁'`	—	—
`ind₁'_lequiv_apply` 📖	mathematical	—	`Ind₁V` `ind₁'_lequiv`	—	—
`ind₁'_lequiv_coind₁'_apply` 📖	mathematical	—	`ind₁'_lequiv_coind₁'`	—	—
`ind₁'_lequiv_coind₁'_comm` 📖	mathematical	—	`ind₁'_lequiv_coind₁'` `ind₁'` `coind₁'`	—	`ind₁'_comp_lsingle`
`ind₁'_lequiv_coind₁'_comm'` 📖	mathematical	—	`ind₁'_lequiv_coind₁'` `coind₁'` `ind₁'`	—	`ind₁'_lequiv_coind₁'_comm`
`ind₁'_lequiv_comm` 📖	mathematical	—	`Ind₁V` `ind₁'_lequiv` `ind₁'` `ind₁`	—	`ind₁'_comp_lsingle` `ind₁'_lequiv_comp_lsingle` `ind₁_apply`
`ind₁'_lequiv_comp_lsingle` 📖	mathematical	—	`Ind₁V` `ind₁'_lequiv`	—	—
`ind₁'_lequiv_symm_apply` 📖	mathematical	—	`Ind₁V` `ind₁'_lequiv` `ind₁'_invlmap`	—	—
`ind₁'_lmap_apply` 📖	mathematical	—	`Ind₁V` `ind₁'_lmap`	—	—
`ind₁'_map_comm` 📖	mathematical	—	`ind₁'_map` `ind₁'`	—	`ind₁'_comp_lsingle`
`ind₁'_π_apply` 📖	mathematical	—	`ind₁'_π`	—	—
`ind₁'_π_comm` 📖	mathematical	—	`ind₁'_π` `ind₁'`	—	—
`ind₁'_π_comp_lsingle` 📖	mathematical	—	`ind₁'_π`	—	—
`ind₁AsFinsupp_apply` 📖	mathematical	—	`ind₁AsFinsupp`	—	`Finsupp.coe_mapDomainLinearEquiv`
`ind₁AsFinsupp_single` 📖	mathematical	—	`ind₁AsFinsupp`	—	—
`ind₁_apply` 📖	mathematical	—	`ind₁`	—	—

Representation.Ind₁V

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

---

← Back to Index