TrivialCohomology

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

Statistics

Metric	Count
Definitions `resCoind₁AsPiIso`, `resCoind₁AsPiLinearEquiv`, `resInd₁AsFinsuppIso`, `resInd₁AsFinsuppLinearEquiv`, `prodQuotEquiv`	5
Theorems `coind₁'_quotientToInvariants_trivialCohomology`, `coind₁_quotientToInvariants_trivialCohomology`, `resCoind₁AsPiLinearEquiv_apply`, `resInd₁AsFinsuppLinearEquiv_apply`, `trivialCohomology_coind₁`, `trivialCohomology_coind₁'`, `trivialCohomology_coind₁AsPi`, `trivialCohomology_ind₁`, `trivialCohomology_ind₁'`, `trivialHomology_coind₁`, `trivialHomology_coind₁'`, `trivialHomology_coind₁AsPi`, `trivialHomology_ind₁`, `trivialHomology_ind₁'`, `trivialHomology_ind₁AsFinsupp`, `trivialTateCohomology_coind₁`, `trivialTateCohomology_coind₁'`, `trivialTateCohomology_coind₁AsPi`, `trivialTateCohomology_ind₁`, `trivialTateCohomology_ind₁'`, `bijective_out_mul`, `prodQuotEquiv_apply`, `prodQuotEquiv_symm_apply`	23
Total	28

Rep

Definitions

Name	Category	Theorems
`resCoind₁AsPiIso` 📖	CompOp	—
`resCoind₁AsPiLinearEquiv` 📖	CompOp	1 math math: `resCoind₁AsPiLinearEquiv_apply`
`resInd₁AsFinsuppIso` 📖	CompOp	—
`resInd₁AsFinsuppLinearEquiv` 📖	CompOp	1 math math: `resInd₁AsFinsuppLinearEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coind₁'_quotientToInvariants_trivialCohomology` 📖	mathematical	—	`TrivialCohomology` `quotientToInvariantsFunctor'` `coind₁'`	—	`coind₁_quotientToInvariants_trivialCohomology` `TrivialCohomology.of_iso`
`coind₁_quotientToInvariants_trivialCohomology` 📖	mathematical	—	`TrivialCohomology` `coind₁` `quotientToInvariantsFunctor'`	—	`TrivialCohomology.of_iso` `trivialCohomology_coind₁`
`resCoind₁AsPiLinearEquiv_apply` 📖	mathematical	—	`resCoind₁AsPiLinearEquiv`	—	—
`resInd₁AsFinsuppLinearEquiv_apply` 📖	mathematical	—	`resInd₁AsFinsuppLinearEquiv`	—	—
`trivialCohomology_coind₁` 📖	mathematical	—	`TrivialCohomology` `coind₁`	—	`TrivialCohomology.of_iso` `trivialCohomology_coind₁AsPi`
`trivialCohomology_coind₁'` 📖	mathematical	—	`TrivialCohomology` `coind₁'`	—	`TrivialCohomology.of_iso` `trivialCohomology_coind₁`
`trivialCohomology_coind₁AsPi` 📖	mathematical	—	`TrivialCohomology` `coind₁AsPi`	—	`isZero_of_trivialCohomology` `instTrivialCohomologyOfSubsingleton`
`trivialCohomology_ind₁` 📖	mathematical	—	`TrivialCohomology` `ind₁`	—	`TrivialCohomology.of_iso` `trivialCohomology_coind₁`
`trivialCohomology_ind₁'` 📖	mathematical	—	`TrivialCohomology` `ind₁'`	—	`TrivialCohomology.of_iso` `trivialCohomology_ind₁`
`trivialHomology_coind₁` 📖	mathematical	—	`TrivialHomology` `coind₁`	—	`TrivialHomology.of_iso` `trivialHomology_ind₁`
`trivialHomology_coind₁'` 📖	mathematical	—	`TrivialCohomology` `coind₁'`	—	`TrivialCohomology.of_iso` `trivialCohomology_coind₁`
`trivialHomology_coind₁AsPi` 📖	mathematical	—	`TrivialHomology` `coind₁AsPi`	—	`TrivialHomology.of_iso` `trivialHomology_coind₁`
`trivialHomology_ind₁` 📖	mathematical	—	`TrivialHomology` `ind₁`	—	`TrivialHomology.of_iso` `trivialHomology_ind₁AsFinsupp`
`trivialHomology_ind₁'` 📖	mathematical	—	`TrivialHomology` `ind₁'`	—	`TrivialHomology.of_iso` `trivialHomology_ind₁`
`trivialHomology_ind₁AsFinsupp` 📖	mathematical	—	`TrivialHomology` `ind₁AsFinsupp`	—	`isZero_of_trivialHomology` `instTrivialHomologyOfSubsingleton`
`trivialTateCohomology_coind₁` 📖	mathematical	—	`TrivialTateCohomology` `coind₁`	—	`TrivialTateCohomology.of_iso` `trivialTateCohomology_coind₁AsPi`
`trivialTateCohomology_coind₁'` 📖	mathematical	—	`TrivialTateCohomology` `coind₁'`	—	`TrivialTateCohomology.of_iso` `trivialTateCohomology_coind₁`
`trivialTateCohomology_coind₁AsPi` 📖	mathematical	—	`TrivialTateCohomology` `coind₁AsPi`	—	`TrivialTateCohomology.of_cases` `trivialCohomology_coind₁AsPi` `trivialHomology_coind₁AsPi`
`trivialTateCohomology_ind₁` 📖	mathematical	—	`TrivialTateCohomology` `ind₁`	—	`TrivialTateCohomology.of_iso` `trivialTateCohomology_coind₁`
`trivialTateCohomology_ind₁'` 📖	mathematical	—	`TrivialTateCohomology` `ind₁'`	—	`TrivialTateCohomology.of_iso` `trivialTateCohomology_ind₁`

(root)

Definitions

Name	Category	Theorems
`prodQuotEquiv` 📖	CompOp	2 math math: `prodQuotEquiv_apply`, `prodQuotEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_out_mul` 📖	—	—	—	—	—
`prodQuotEquiv_apply` 📖	mathematical	—	`prodQuotEquiv`	—	—
`prodQuotEquiv_symm_apply` 📖	mathematical	—	`prodQuotEquiv` `bijective_out_mul`	—	—

---

← Back to Index