Documentation Verification Report

TateCohomology

📁 Source: ClassFieldTheory/Cohomology/TateCohomology.lean

Statistics

Metric	Count
Definitions `cochainsMap`, `isoGroupCohomology`, `isoGroupHomology`, `map`, `negOneIso`, `isoShortComplexHneg1`, `sc`, `negOneIsoOfIsTrivial`, `res_iso`, `eval_neg`, `eval_nonneg`, `zeroIso`, `isoShortComplexH0`, `sc`, `zeroIsoOfIsTrivial`, `zeroTrivialInt`, `δ`, `tateCohomology`, `tateComplex`, `map`, `normNatEnd`, `tateComplexConnectData`, `tateComplexFunctor`, `tateNorm`	24
Theorems `exact₁`, `exact₃`, `instAdditiveRepCochainComplexModuleCatIntTateComplexFunctor`, `instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor`, `instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1`, `isZero_neg_one_trivial_of_isAddTorsionFree`, `map_tateComplexFunctor_shortExact`, `map_δ`, `isoShortComplexHneg1_hom_τ₁_hom_apply_apply`, `isoShortComplexHneg1_hom_τ₁_hom_apply_support_val`, `isoShortComplexHneg1_hom_τ₂_hom_apply`, `isoShortComplexHneg1_hom_τ₃_hom_apply`, `isoShortComplexHneg1_inv_τ₁_hom_apply`, `isoShortComplexHneg1_inv_τ₂_hom_apply_apply`, `isoShortComplexHneg1_inv_τ₂_hom_apply_support_val`, `isoShortComplexHneg1_inv_τ₃_hom_apply`, `sc_X₁_carrier`, `sc_X₁_isAddCommGroup`, `sc_X₁_isModule`, `sc_X₂`, `sc_X₃`, `sc_f`, `sc_g`, `preservesFiniteColimits_tateComplexFunctor`, `preservesFiniteLimits_tateComplexFunctor`, `isoShortComplexH0_hom_τ₁_hom_apply`, `isoShortComplexH0_hom_τ₂_hom_apply`, `isoShortComplexH0_hom_τ₃_hom_apply`, `isoShortComplexH0_inv_τ₁_hom_apply`, `isoShortComplexH0_inv_τ₂_hom_apply`, `isoShortComplexH0_inv_τ₃_hom_apply`, `sc_X₁`, `sc_X₂`, `sc_X₃_carrier`, `sc_X₃_isAddCommGroup`, `sc_X₃_isModule`, `sc_f`, `sc_g`, `δ_map`, `comp_eq_zero`, `d_comp_tateNorm`, `norm_comp_d_eq_zero`, `norm_comp_d_eq_zero_apply`, `norm_comp_d_eq_zero_assoc`, `map_zero`, `norm_comm`, `norm_comm_assoc`, `norm_hom_comm`, `norm_hom_comm_assoc`, `tateComplexConnectData_d₀`, `tateComplexFunctor_map`, `tateComplexFunctor_obj`, `tateComplex_X`, `tateComplex_d_neg`, `tateComplex_d_neg_one`, `tateComplex_d_ofNat`, `tateNorm_comp_d`, `tateNorm_eq`, `tateNorm_hom_apply`	59
Total	83

groupCohomology

Definitions

Name	Category	Theorems
`tateCohomology` 📖	CompOp	16 math math: `TateCohomology.isZero_odd_trivial_of_isAddTorsionFree`, `TateCohomology.isIso_δ`, `Rep.TrivialTateCohomology.isZero`, `TateCohomology.exact₃`, `δDownIsoTate_hom`, `Rep.aug.tateCohomology_auc_succ_iso`, `Rep.isZero_of_trivialTateCohomology`, `TateCohomology.isZero_neg_one_trivial_of_isAddTorsionFree`, `TateCohomology.exact₁`, `δUpIsoTate_hom`, `Rep.TrivialTateCohomology.of_injective`, `Rep.split.isIso_δ`, `TateCohomology.δ_map`, `instIsIso_shortExact_upSES`, `instIsIso_shortExact_downSES`, `TateCohomology.map_δ`
`tateComplex` 📖	CompOp	20 math math: `TateCohomology.negOneIso.isoShortComplexHneg1_hom_τ₁_hom_apply_support_val`, `TateCohomology.zeroIso.isoShortComplexH0_inv_τ₁_hom_apply`, `TateCohomology.zeroIso.isoShortComplexH0_hom_τ₁_hom_apply`, `TateCohomology.zeroIso.isoShortComplexH0_inv_τ₃_hom_apply`, `tateComplex.map_zero`, `tateComplex_d_ofNat`, `TateCohomology.negOneIso.isoShortComplexHneg1_inv_τ₃_hom_apply`, `tateComplex_d_neg_one`, `TateCohomology.negOneIso.isoShortComplexHneg1_hom_τ₁_hom_apply_apply`, `TateCohomology.zeroIso.isoShortComplexH0_hom_τ₂_hom_apply`, `TateCohomology.negOneIso.isoShortComplexHneg1_inv_τ₂_hom_apply_apply`, `tateComplexFunctor_obj`, `TateCohomology.negOneIso.isoShortComplexHneg1_inv_τ₂_hom_apply_support_val`, `TateCohomology.negOneIso.isoShortComplexHneg1_inv_τ₁_hom_apply`, `tateComplex_d_neg`, `TateCohomology.negOneIso.isoShortComplexHneg1_hom_τ₂_hom_apply`, `TateCohomology.negOneIso.isoShortComplexHneg1_hom_τ₃_hom_apply`, `TateCohomology.zeroIso.isoShortComplexH0_inv_τ₂_hom_apply`, `TateCohomology.zeroIso.isoShortComplexH0_hom_τ₃_hom_apply`, `tateComplex_X`
`tateComplexConnectData` 📖	CompOp	1 math math: `tateComplexConnectData_d₀`
`tateComplexFunctor` 📖	CompOp	8 math math: `TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1`, `TateCohomology.preservesFiniteLimits_tateComplexFunctor`, `TateCohomology.instAdditiveRepCochainComplexModuleCatIntTateComplexFunctor`, `tateComplexFunctor_obj`, `TateCohomology.map_tateComplexFunctor_shortExact`, `tateComplexFunctor_map`, `TateCohomology.preservesFiniteColimits_tateComplexFunctor`, `TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor`
`tateNorm` 📖	CompOp	6 math math: `tateNorm_eq`, `tateNorm_comp_d`, `tateComplex_d_neg_one`, `tateComplexConnectData_d₀`, `tateNorm_hom_apply`, `d_comp_tateNorm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq_zero` 📖	—	—	—	—	—
`d_comp_tateNorm` 📖	mathematical	—	`tateNorm`	—	`comp_eq_zero`
`norm_comp_d_eq_zero` 📖	—	—	—	—	—
`norm_comp_d_eq_zero_apply` 📖	—	—	—	—	`norm_comp_d_eq_zero`
`norm_comp_d_eq_zero_assoc` 📖	—	—	—	—	`norm_comp_d_eq_zero`
`tateComplexConnectData_d₀` 📖	mathematical	—	`tateComplexConnectData` `tateNorm`	—	—
`tateComplexFunctor_map` 📖	mathematical	—	`tateComplexFunctor` `tateComplex.map`	—	—
`tateComplexFunctor_obj` 📖	mathematical	—	`tateComplexFunctor` `tateComplex`	—	—
`tateComplex_X` 📖	mathematical	—	`tateComplex`	—	—
`tateComplex_d_neg` 📖	mathematical	—	`tateComplex`	—	—
`tateComplex_d_neg_one` 📖	mathematical	—	`tateComplex` `tateNorm`	—	—
`tateComplex_d_ofNat` 📖	mathematical	—	`tateComplex`	—	—
`tateNorm_comp_d` 📖	mathematical	—	`tateNorm`	—	`norm_comp_d_eq_zero_assoc`
`tateNorm_eq` 📖	mathematical	—	`tateNorm`	—	—
`tateNorm_hom_apply` 📖	mathematical	—	`tateNorm`	—	—

groupCohomology.TateCohomology

Definitions

Name	Category	Theorems
`cochainsMap` 📖	CompOp	—
`isoGroupCohomology` 📖	CompOp	—
`isoGroupHomology` 📖	CompOp	—
`map` 📖	CompOp	—
`negOneIso` 📖	CompOp	—
`negOneIsoOfIsTrivial` 📖	CompOp	—
`res_iso` 📖	CompOp	—
`zeroIso` 📖	CompOp	—
`zeroIsoOfIsTrivial` 📖	CompOp	—
`zeroTrivialInt` 📖	CompOp	—
`δ` 📖	CompOp	11 math math: `TateCohomology.isIso_δ`, `exact₃`, `groupCohomology.δDownIsoTate_hom`, `Rep.aug.tateCohomology_auc_succ_iso`, `exact₁`, `groupCohomology.δUpIsoTate_hom`, `Rep.split.isIso_δ`, `δ_map`, `groupCohomology.instIsIso_shortExact_upSES`, `groupCohomology.instIsIso_shortExact_downSES`, `map_δ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exact₁` 📖	mathematical	—	`groupCohomology.tateCohomology` `δ` `δ_map`	—	`instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1` `map_tateComplexFunctor_shortExact`
`exact₃` 📖	mathematical	—	`groupCohomology.tateCohomology` `δ` `map_δ`	—	`instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1` `map_tateComplexFunctor_shortExact`
`instAdditiveRepCochainComplexModuleCatIntTateComplexFunctor` 📖	mathematical	—	`groupCohomology.tateComplexFunctor`	—	—
`instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor` 📖	mathematical	—	`groupCohomology.tateComplexFunctor`	—	`groupCohomology.tateComplex.map_zero`
`instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1` 📖	mathematical	—	`groupCohomology.tateComplexFunctor`	—	`groupCohomology.tateComplex.map_zero`
`isZero_neg_one_trivial_of_isAddTorsionFree` 📖	mathematical	—	`groupCohomology.tateCohomology`	—	—
`map_tateComplexFunctor_shortExact` 📖	mathematical	—	`groupCohomology.tateComplexFunctor` `instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1`	—	`instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1` `CategoryTheory.ShortComplex.ShortExact.map_of_natIso` `groupCohomology.map_cochainsFunctor_eval_shortExact` `groupHomology.map_chainsFunctor_eval_shortExact`
`map_δ` 📖	mathematical	—	`groupCohomology.tateCohomology` `δ`	—	`instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1` `map_tateComplexFunctor_shortExact`
`preservesFiniteColimits_tateComplexFunctor` 📖	mathematical	—	`groupCohomology.tateComplexFunctor`	—	`instAdditiveRepCochainComplexModuleCatIntTateComplexFunctor` `map_tateComplexFunctor_shortExact`
`preservesFiniteLimits_tateComplexFunctor` 📖	mathematical	—	`groupCohomology.tateComplexFunctor`	—	`instAdditiveRepCochainComplexModuleCatIntTateComplexFunctor` `map_tateComplexFunctor_shortExact`
`δ_map` 📖	mathematical	—	`groupCohomology.tateCohomology` `δ`	—	`instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1` `map_tateComplexFunctor_shortExact`

groupCohomology.TateCohomology.negOneIso

Definitions

Name	Category	Theorems
`isoShortComplexHneg1` 📖	CompOp	8 math math: `isoShortComplexHneg1_hom_τ₁_hom_apply_support_val`, `isoShortComplexHneg1_inv_τ₃_hom_apply`, `isoShortComplexHneg1_hom_τ₁_hom_apply_apply`, `isoShortComplexHneg1_inv_τ₂_hom_apply_apply`, `isoShortComplexHneg1_inv_τ₂_hom_apply_support_val`, `isoShortComplexHneg1_inv_τ₁_hom_apply`, `isoShortComplexHneg1_hom_τ₂_hom_apply`, `isoShortComplexHneg1_hom_τ₃_hom_apply`
`sc` 📖	CompOp	15 math math: `isoShortComplexHneg1_hom_τ₁_hom_apply_support_val`, `isoShortComplexHneg1_inv_τ₃_hom_apply`, `isoShortComplexHneg1_hom_τ₁_hom_apply_apply`, `isoShortComplexHneg1_inv_τ₂_hom_apply_apply`, `isoShortComplexHneg1_inv_τ₂_hom_apply_support_val`, `isoShortComplexHneg1_inv_τ₁_hom_apply`, `isoShortComplexHneg1_hom_τ₂_hom_apply`, `sc_X₁_isModule`, `sc_f`, `sc_g`, `sc_X₂`, `isoShortComplexHneg1_hom_τ₃_hom_apply`, `sc_X₁_isAddCommGroup`, `sc_X₃`, `sc_X₁_carrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isoShortComplexHneg1_hom_τ₁_hom_apply_apply` 📖	mathematical	—	`groupCohomology.tateComplex` `sc` `isoShortComplexHneg1`	—	—
`isoShortComplexHneg1_hom_τ₁_hom_apply_support_val` 📖	mathematical	—	`groupCohomology.tateComplex` `sc` `isoShortComplexHneg1`	—	—
`isoShortComplexHneg1_hom_τ₂_hom_apply` 📖	mathematical	—	`groupCohomology.tateComplex` `sc` `isoShortComplexHneg1`	—	—
`isoShortComplexHneg1_hom_τ₃_hom_apply` 📖	mathematical	—	`groupCohomology.tateComplex` `sc` `isoShortComplexHneg1`	—	—
`isoShortComplexHneg1_inv_τ₁_hom_apply` 📖	mathematical	—	`sc` `groupCohomology.tateComplex` `isoShortComplexHneg1`	—	—
`isoShortComplexHneg1_inv_τ₂_hom_apply_apply` 📖	mathematical	—	`sc` `groupCohomology.tateComplex` `isoShortComplexHneg1`	—	—
`isoShortComplexHneg1_inv_τ₂_hom_apply_support_val` 📖	mathematical	—	`sc` `groupCohomology.tateComplex` `isoShortComplexHneg1`	—	—
`isoShortComplexHneg1_inv_τ₃_hom_apply` 📖	mathematical	—	`sc` `groupCohomology.tateComplex` `isoShortComplexHneg1`	—	—
`sc_X₁_carrier` 📖	mathematical	—	`sc`	—	—
`sc_X₁_isAddCommGroup` 📖	mathematical	—	`sc`	—	—
`sc_X₁_isModule` 📖	mathematical	—	`sc`	—	—
`sc_X₂` 📖	mathematical	—	`sc`	—	—
`sc_X₃` 📖	mathematical	—	`sc`	—	—
`sc_f` 📖	mathematical	—	`sc`	—	—
`sc_g` 📖	mathematical	—	`sc`	—	—

groupCohomology.TateCohomology.tateComplex

Definitions

Name	Category	Theorems
`eval_neg` 📖	CompOp	—
`eval_nonneg` 📖	CompOp	—

groupCohomology.TateCohomology.zeroIso

Definitions

Name	Category	Theorems
`isoShortComplexH0` 📖	CompOp	6 math math: `isoShortComplexH0_inv_τ₁_hom_apply`, `isoShortComplexH0_hom_τ₁_hom_apply`, `isoShortComplexH0_inv_τ₃_hom_apply`, `isoShortComplexH0_hom_τ₂_hom_apply`, `isoShortComplexH0_inv_τ₂_hom_apply`, `isoShortComplexH0_hom_τ₃_hom_apply`
`sc` 📖	CompOp	13 math math: `sc_X₃_carrier`, `isoShortComplexH0_inv_τ₁_hom_apply`, `isoShortComplexH0_hom_τ₁_hom_apply`, `isoShortComplexH0_inv_τ₃_hom_apply`, `sc_X₂`, `sc_X₃_isModule`, `isoShortComplexH0_hom_τ₂_hom_apply`, `sc_g`, `sc_X₃_isAddCommGroup`, `sc_X₁`, `isoShortComplexH0_inv_τ₂_hom_apply`, `isoShortComplexH0_hom_τ₃_hom_apply`, `sc_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isoShortComplexH0_hom_τ₁_hom_apply` 📖	mathematical	—	`groupCohomology.tateComplex` `sc` `isoShortComplexH0`	—	—
`isoShortComplexH0_hom_τ₂_hom_apply` 📖	mathematical	—	`groupCohomology.tateComplex` `sc` `isoShortComplexH0`	—	—
`isoShortComplexH0_hom_τ₃_hom_apply` 📖	mathematical	—	`groupCohomology.tateComplex` `sc` `isoShortComplexH0`	—	—
`isoShortComplexH0_inv_τ₁_hom_apply` 📖	mathematical	—	`sc` `groupCohomology.tateComplex` `isoShortComplexH0`	—	—
`isoShortComplexH0_inv_τ₂_hom_apply` 📖	mathematical	—	`sc` `groupCohomology.tateComplex` `isoShortComplexH0`	—	—
`isoShortComplexH0_inv_τ₃_hom_apply` 📖	mathematical	—	`sc` `groupCohomology.tateComplex` `isoShortComplexH0`	—	—
`sc_X₁` 📖	mathematical	—	`sc`	—	—
`sc_X₂` 📖	mathematical	—	`sc`	—	—
`sc_X₃_carrier` 📖	mathematical	—	`sc`	—	—
`sc_X₃_isAddCommGroup` 📖	mathematical	—	`sc`	—	—
`sc_X₃_isModule` 📖	mathematical	—	`sc`	—	—
`sc_f` 📖	mathematical	—	`sc`	—	—
`sc_g` 📖	mathematical	—	`sc`	—	—

groupCohomology.tateComplex

Definitions

Name	Category	Theorems
`map` 📖	CompOp	2 math math: `map_zero`, `groupCohomology.tateComplexFunctor_map`
`normNatEnd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_zero` 📖	mathematical	—	`map` `groupCohomology.tateComplex`	—	—
`norm_comm` 📖	—	—	—	—	—
`norm_comm_assoc` 📖	—	—	—	—	`norm_comm`
`norm_hom_comm` 📖	—	—	—	—	`norm_comm`
`norm_hom_comm_assoc` 📖	—	—	—	—	`norm_hom_comm`

---

← Back to Index