UpDown

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

Statistics

Metric	Count
Definitions map₁, map₂, periodSeq₁, periodSeq₁Functor, periodSeq₂, periodSeq₂Functor, periodicCohomology, periodicCohomologyAux, upIsoDown, map₁, map₂, evenTrivialInt, evenTrivialInt, oddTrivialInt, periodicTateCohomology, periodicTateCohomologyAux	16
Theorems coind_ι_gg_map₁, coind_ι_gg_map₁_app, exact_periodSeq₁, exact_periodSeq₂, isZero_ofEven_odd, map₁_comp_ind₁'_iso_coind₁', map₂_app_gg_ind₁'_π_app, map₂_gg_ind₁'_π, periodSeq₁Functor_map, periodSeq₁Functor_obj, periodSeq₁_X₁, periodSeq₁_X₂, periodSeq₁_X₃, periodSeq₁_f, periodSeq₁_g, periodSeq₂Functor_map, periodSeq₂Functor_obj, periodSeq₂_X₁, periodSeq₂_X₂, periodSeq₂_X₃, periodSeq₂_f, periodSeq₂_g, ind₁'_π_comp_map₂, map₁_apply, map₁_comm, map₁_comp_coind_ι, map₁_ker, map₂_apply, map₂_apply_apply, map₂_apply_support, map₂_comm, map₂_comp_lsingle, map₂_range, isZero_odd_trivial_of_isAddTorsionFree, isZero_odd_trivial_of_isAddTorsionFree, isZero_even_trivial_of_isAddTorsionFree, ofHom_add, ofHom_one, ofHom_sub, ofHom_zero	40
Total	56

Rep

Definitions

Name	Category	Theorems
map₁ 📖	CompOp	5 math math: map₁_comp_ind₁'_iso_coind₁', coind_ι_gg_map₁_app, periodSeq₂_f, periodSeq₁_g, coind_ι_gg_map₁
map₂ 📖	CompOp	3 math math: map₁_comp_ind₁'_iso_coind₁', map₂_gg_ind₁'_π, map₂_app_gg_ind₁'_π_app
periodSeq₁ 📖	CompOp	8 math math: periodSeq₁_f, periodSeq₁_X₂, periodSeq₁_X₃, periodSeq₁Functor_map, periodSeq₁_g, exact_periodSeq₁, periodSeq₁_X₁, periodSeq₁Functor_obj
periodSeq₁Functor 📖	CompOp	2 math math: periodSeq₁Functor_map, periodSeq₁Functor_obj
periodSeq₂ 📖	CompOp	8 math math: exact_periodSeq₂, periodSeq₂Functor_obj, periodSeq₂_f, periodSeq₂Functor_map, periodSeq₂_X₁, periodSeq₂_g, periodSeq₂_X₃, periodSeq₂_X₂
periodSeq₂Functor 📖	CompOp	2 math math: periodSeq₂Functor_obj, periodSeq₂Functor_map
periodicCohomology 📖	CompOp	—
periodicCohomologyAux 📖	CompOp	—
upIsoDown 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coind_ι_gg_map₁ 📖	mathematical	—	coind₁' coind₁'_ι map₁	—	coind_ι_gg_map₁_app
coind_ι_gg_map₁_app 📖	mathematical	—	coind₁' coind₁'_ι map₁	—	Representation.map₁_comp_coind_ι
exact_periodSeq₁ 📖	mathematical	—	periodSeq₁	—	CategoryTheory.ShortComplex.Exact.moduleCat_of_ker_le_range
exact_periodSeq₂ 📖	mathematical	—	periodSeq₂	—	CategoryTheory.ShortComplex.Exact.moduleCat_of_ker_le_range Representation.map₂_range Representation.map₂_apply
isZero_ofEven_odd 📖	—	—	—	—	—
map₁_comp_ind₁'_iso_coind₁' 📖	mathematical	—	coind₁' ind₁' map₁ ind₁'_iso_coind₁' map₂	—	Representation.map₂_apply
map₂_app_gg_ind₁'_π_app 📖	mathematical	—	ind₁' map₂ ind₁'_π	—	Representation.ind₁'_π_comp_map₂
map₂_gg_ind₁'_π 📖	mathematical	—	ind₁' map₂ ind₁'_π	—	map₂_app_gg_ind₁'_π_app
periodSeq₁Functor_map 📖	mathematical	—	periodSeq₁Functor periodSeq₁ coind₁' ind₁'	—	—
periodSeq₁Functor_obj 📖	mathematical	—	periodSeq₁Functor periodSeq₁	—	—
periodSeq₁_X₁ 📖	mathematical	—	periodSeq₁	—	—
periodSeq₁_X₂ 📖	mathematical	—	periodSeq₁ coind₁'	—	—
periodSeq₁_X₃ 📖	mathematical	—	periodSeq₁ ind₁'	—	—
periodSeq₁_f 📖	mathematical	—	periodSeq₁ coind₁' coind₁'_ι	—	—
periodSeq₁_g 📖	mathematical	—	periodSeq₁ coind₁' ind₁' map₁ ind₁'_iso_coind₁'	—	—
periodSeq₂Functor_map 📖	mathematical	—	periodSeq₂Functor periodSeq₂ coind₁' ind₁'	—	—
periodSeq₂Functor_obj 📖	mathematical	—	periodSeq₂Functor periodSeq₂	—	—
periodSeq₂_X₁ 📖	mathematical	—	periodSeq₂ coind₁'	—	—
periodSeq₂_X₂ 📖	mathematical	—	periodSeq₂ ind₁'	—	—
periodSeq₂_X₃ 📖	mathematical	—	periodSeq₂	—	—
periodSeq₂_f 📖	mathematical	—	periodSeq₂ coind₁' ind₁' map₁ ind₁'_iso_coind₁'	—	—
periodSeq₂_g 📖	mathematical	—	periodSeq₂ ind₁' ind₁'_π	—	—

Representation

Definitions

Name	Category	Theorems
map₁ 📖	CompOp	4 math math: map₁_ker, map₁_comp_coind_ι, map₁_apply, map₁_comm
map₂ 📖	CompOp	7 math math: map₂_comm, ind₁'_π_comp_map₂, map₂_range, map₂_apply_apply, map₂_apply_support, map₂_apply, map₂_comp_lsingle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ind₁'_π_comp_map₂ 📖	mathematical	—	ind₁'_π map₂	—	map₂_comp_lsingle ind₁'_π_comp_lsingle
map₁_apply 📖	mathematical	—	map₁ IsCyclic.gen	—	—
map₁_comm 📖	mathematical	—	map₁ coind₁'	—	—
map₁_comp_coind_ι 📖	mathematical	—	map₁ coind₁'_ι	—	—
map₁_ker 📖	mathematical	—	map₁ coind₁'_ι	—	IsCyclic.gen_generate map₁_comp_coind_ι
map₂_apply 📖	mathematical	—	map₂ IsCyclic.gen	—	—
map₂_apply_apply 📖	mathematical	—	map₂ IsCyclic.gen	—	—
map₂_apply_support 📖	mathematical	—	map₂ IsCyclic.gen	—	—
map₂_comm 📖	mathematical	—	map₂ ind₁'	—	ind₁'_comp_lsingle map₂_comp_lsingle
map₂_comp_lsingle 📖	mathematical	—	map₂ IsCyclic.gen	—	—
map₂_range 📖	mathematical	—	map₂ ind₁'_π	—	ind₁'_π_comp_map₂ IsCyclic.unique_gen_pow map₂_apply

(root)

Definitions

Name	Category	Theorems
periodicTateCohomology 📖	CompOp	—
periodicTateCohomologyAux 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofHom_add 📖	—	—	—	—	—
ofHom_one 📖	—	—	—	—	—
ofHom_sub 📖	—	—	—	—	—
ofHom_zero 📖	—	—	—	—	—

groupCohomology

Definitions

Name	Category	Theorems
evenTrivialInt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero_odd_trivial_of_isAddTorsionFree 📖	—	—	—	—	TateCohomology.isZero_odd_trivial_of_isAddTorsionFree

groupCohomology.TateCohomology

Definitions

Name	Category	Theorems
evenTrivialInt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero_odd_trivial_of_isAddTorsionFree 📖	mathematical	—	groupCohomology.tateCohomology	—	isZero_neg_one_trivial_of_isAddTorsionFree

groupHomology

Definitions

Name	Category	Theorems
oddTrivialInt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isZero_even_trivial_of_isAddTorsionFree 📖	—	—	—	—	groupCohomology.TateCohomology.isZero_odd_trivial_of_isAddTorsionFree

---

← Back to Index