UpDown

📁 Source: ClassFieldTheory/Cohomology/Functors/UpDown.lean

Statistics

Metric	Count
Definitions `down`, `ι`, `downSES`, `downShortComplex`, `up`, `π`, `upSES`, `upShortComplex`, `δDownIso`, `δDownNatIso`, `δDownResIso`, `δUpIso`, `δUpNatIso`, `δUpResIso`, `δDownIsoTate`, `δDownNatIsoTate`, `δDownResIsoTate`, `δUpIsoTate`, `δUpNatIsoTate`, `δUpResIsoTate`	20
Theorems `downSES_X₁`, `downSES_X₂`, `downSES_X₃`, `downSES_f`, `downSES_g`, `downShortComplex_map_τ₁`, `downShortComplex_map_τ₂`, `downShortComplex_map_τ₃`, `downShortComplex_obj`, `down_map`, `down_obj`, `epi_δ_down_res_zero`, `epi_δ_down_zero`, `epi_δ_up_zero_res`, `isIso_δ_down`, `isIso_δ_down_res`, `isIso_δ_up_res`, `shortExact_downSES`, `shortExact_downSES_res`, `shortExact_upSES`, `shortExact_upSES_res`, `upSES_X₁`, `upSES_X₂`, `upSES_X₃`, `upSES_f`, `upSES_g`, `upShortComplex_map_τ₁`, `upShortComplex_map_τ₂`, `upShortComplex_map_τ₃`, `upShortComplex_obj`, `up_map`, `up_obj`, `δUpIso_hom`, `δ_up_isIso`, `δ_up_zero_epi`, `instIsIso_shortExact_downSES`, `instIsIso_shortExact_upSES`, `δDownIsoTate_hom`, `δUpIsoTate_hom`	39
Total	59
⚠️ With sorry `δDownResIsoTate`, `δUpResIsoTate`	2

Rep.dimensionShift

Definitions

Name	Category	Theorems
`down` 📖	CompOp	6 math math: `down_trivialCohomology`, `down_map`, `downShortComplex_map_τ₁`, `downSES_X₁`, `groupCohomology.δDownIsoTate_hom`, `down_obj`
`downSES` 📖	CompOp	17 math math: `downSES_X₂`, `downShortComplex_map_τ₁`, `downSES_X₁`, `downShortComplex_obj`, `isIso_δ_down_res`, `groupCohomology.δDownIsoTate_hom`, `epi_δ_down_res_zero`, `isIso_δ_down`, `downShortComplex_map_τ₂`, `downSES_X₃`, `epi_δ_down_zero`, `shortExact_downSES_res`, `downShortComplex_map_τ₃`, `shortExact_downSES`, `downSES_f`, `downSES_g`, `groupCohomology.instIsIso_shortExact_downSES`
`downShortComplex` 📖	CompOp	4 math math: `downShortComplex_map_τ₁`, `downShortComplex_obj`, `downShortComplex_map_τ₂`, `downShortComplex_map_τ₃`
`up` 📖	CompOp	8 math math: `up_map`, `groupCohomology.commSqₙ`, `δUpIso_hom`, `up_obj`, `upSES_X₃`, `upShortComplex_map_τ₃`, `groupCohomology.δUpIsoTate_hom`, `up_trivialCohomology`
`upSES` 📖	CompOp	21 math math: `upSES_X₂`, `upSES_f`, `upSES_g`, `upShortComplex_obj`, `groupCohomology.commSqₙ`, `δ_up_isIso`, `δUpIso_hom`, `isIso_δ_up_res`, `upSES_X₃`, `δ_up_zero_epi`, `groupCohomology.commSq_cores₁`, `upShortComplex_map_τ₁`, `epi_δ_up_zero_res`, `upShortComplex_map_τ₃`, `upSES_X₁`, `groupCohomology.δUpIsoTate_hom`, `shortExact_upSES_res`, `groupCohomology.commSq_cores₁_assoc`, `upShortComplex_map_τ₂`, `groupCohomology.instIsIso_shortExact_upSES`, `shortExact_upSES`
`upShortComplex` 📖	CompOp	4 math math: `upShortComplex_obj`, `upShortComplex_map_τ₁`, `upShortComplex_map_τ₃`, `upShortComplex_map_τ₂`
`δDownIso` 📖	CompOp	—
`δDownNatIso` 📖	CompOp	—
`δDownResIso` 📖	CompOp	—
`δUpIso` 📖	CompOp	1 math math: `δUpIso_hom`
`δUpNatIso` 📖	CompOp	—
`δUpResIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`downSES_X₁` 📖	mathematical	—	`downSES` `down`	—	—
`downSES_X₂` 📖	mathematical	—	`downSES` `Rep.ind₁'`	—	—
`downSES_X₃` 📖	mathematical	—	`downSES`	—	—
`downSES_f` 📖	mathematical	—	`downSES` `down.ι`	—	—
`downSES_g` 📖	mathematical	—	`downSES` `Rep.ind₁'` `Rep.ind₁'_π`	—	—
`downShortComplex_map_τ₁` 📖	mathematical	—	`downSES` `downShortComplex` `down`	—	—
`downShortComplex_map_τ₂` 📖	mathematical	—	`downSES` `downShortComplex` `Rep.ind₁'`	—	—
`downShortComplex_map_τ₃` 📖	mathematical	—	`downSES` `downShortComplex`	—	—
`downShortComplex_obj` 📖	mathematical	—	`downShortComplex` `downSES`	—	—
`down_map` 📖	mathematical	—	`down` `Rep.ind₁'` `Rep.ind₁'_π`	—	—
`down_obj` 📖	mathematical	—	`down` `Rep.ind₁'` `Rep.ind₁'_π`	—	—
`epi_δ_down_res_zero` 📖	mathematical	—	`downSES` `Rep.res` `Rep.instAdditiveRes` `shortExact_downSES_res`	—	`Rep.instAdditiveRes` `shortExact_downSES_res` `Rep.isZero_of_injective` `Rep.trivialCohomology_ind₁'`
`epi_δ_down_zero` 📖	mathematical	—	`downSES` `shortExact_downSES`	—	`shortExact_downSES` `Rep.isZero_of_trivialCohomology` `Rep.trivialCohomology_ind₁'`
`epi_δ_up_zero_res` 📖	mathematical	—	`upSES` `Rep.res` `Rep.instAdditiveRes` `Rep.shortExact_res` `shortExact_upSES`	—	`Rep.instAdditiveRes` `Rep.shortExact_res` `shortExact_upSES` `Rep.isZero_of_injective` `Rep.trivialHomology_coind₁'`
`isIso_δ_down` 📖	mathematical	—	`downSES` `shortExact_downSES`	—	`shortExact_downSES` `Rep.isZero_of_trivialCohomology` `Rep.trivialCohomology_ind₁'`
`isIso_δ_down_res` 📖	mathematical	—	`downSES` `Rep.res` `Rep.instAdditiveRes` `shortExact_downSES_res`	—	`Rep.instAdditiveRes` `shortExact_downSES_res` `Rep.isZero_of_injective` `Rep.trivialCohomology_ind₁'`
`isIso_δ_up_res` 📖	mathematical	—	`upSES` `Rep.res` `Rep.instAdditiveRes` `Rep.shortExact_res` `shortExact_upSES`	—	`Rep.instAdditiveRes` `Rep.shortExact_res` `shortExact_upSES` `Rep.isZero_of_injective` `Rep.trivialHomology_coind₁'`
`shortExact_downSES` 📖	mathematical	—	`downSES`	—	`Rep.instEpiAppInd₁'_π`
`shortExact_downSES_res` 📖	mathematical	—	`downSES` `Rep.res` `Rep.instAdditiveRes`	—	`Rep.instAdditiveRes` `shortExact_downSES`
`shortExact_upSES` 📖	mathematical	—	`upSES`	—	`Rep.instMonoAppCoind₁'_ι`
`shortExact_upSES_res` 📖	mathematical	—	`upSES` `Rep.res` `Rep.instAdditiveRes`	—	`Rep.instAdditiveRes` `shortExact_upSES`
`upSES_X₁` 📖	mathematical	—	`upSES`	—	—
`upSES_X₂` 📖	mathematical	—	`upSES` `Rep.coind₁'`	—	—
`upSES_X₃` 📖	mathematical	—	`upSES` `up`	—	—
`upSES_f` 📖	mathematical	—	`upSES` `Rep.coind₁'` `Rep.coind₁'_ι`	—	—
`upSES_g` 📖	mathematical	—	`upSES` `up.π`	—	—
`upShortComplex_map_τ₁` 📖	mathematical	—	`upSES` `upShortComplex`	—	—
`upShortComplex_map_τ₂` 📖	mathematical	—	`upSES` `upShortComplex` `Rep.coind₁'`	—	—
`upShortComplex_map_τ₃` 📖	mathematical	—	`upSES` `upShortComplex` `up`	—	—
`upShortComplex_obj` 📖	mathematical	—	`upShortComplex` `upSES`	—	—
`up_map` 📖	mathematical	—	`up` `Rep.coind₁'` `Rep.coind₁'_ι`	—	—
`up_obj` 📖	mathematical	—	`up` `Rep.coind₁'` `Rep.coind₁'_ι`	—	—
`δUpIso_hom` 📖	mathematical	—	`up` `δUpIso` `upSES` `shortExact_upSES`	—	—
`δ_up_isIso` 📖	mathematical	—	`upSES` `shortExact_upSES`	—	`shortExact_upSES` `Rep.isZero_of_trivialCohomology` `Rep.trivialHomology_coind₁'`
`δ_up_zero_epi` 📖	mathematical	—	`upSES` `shortExact_upSES`	—	`shortExact_upSES` `Rep.isZero_of_trivialCohomology` `Rep.trivialHomology_coind₁'`

Rep.dimensionShift.down

Definitions

Name	Category	Theorems
`ι` 📖	CompOp	1 math math: `Rep.dimensionShift.downSES_f`

Rep.dimensionShift.up

Definitions

Name	Category	Theorems
`π` 📖	CompOp	1 math math: `Rep.dimensionShift.upSES_g`

groupCohomology

Definitions

Name	Category	Theorems
`δDownIsoTate` 📖	CompOp	1 math math: `δDownIsoTate_hom`
`δDownNatIsoTate` 📖	CompOp	—
`δDownResIsoTate` 📖 ⚠️	CompOp	—
`δUpIsoTate` 📖	CompOp	1 math math: `δUpIsoTate_hom`
`δUpNatIsoTate` 📖	CompOp	—
`δUpResIsoTate` 📖 ⚠️	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIso_shortExact_downSES` 📖	mathematical	—	`tateCohomology` `Rep.dimensionShift.downSES` `TateCohomology.δ` `Rep.dimensionShift.shortExact_downSES`	—	`Rep.trivialTateCohomology_ind₁'` `TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1` `TateCohomology.map_tateComplexFunctor_shortExact` `Rep.dimensionShift.shortExact_downSES`
`instIsIso_shortExact_upSES` 📖	mathematical	—	`tateCohomology` `Rep.dimensionShift.upSES` `TateCohomology.δ` `Rep.dimensionShift.shortExact_upSES`	—	`Rep.trivialTateCohomology_coind₁'` `TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1` `TateCohomology.map_tateComplexFunctor_shortExact` `Rep.dimensionShift.shortExact_upSES`
`δDownIsoTate_hom` 📖	mathematical	—	`tateCohomology` `Rep.dimensionShift.down` `δDownIsoTate` `TateCohomology.δ` `Rep.dimensionShift.downSES` `Rep.dimensionShift.shortExact_downSES`	—	—
`δUpIsoTate_hom` 📖	mathematical	—	`tateCohomology` `Rep.dimensionShift.up` `δUpIsoTate` `TateCohomology.δ` `Rep.dimensionShift.upSES` `Rep.dimensionShift.shortExact_upSES`	—	—

---

← Back to Index