Connect

📁 Source: Mathlib/Algebra/Homology/Embedding/Connect.lean

Statistics

Metric	Count
Definitions ConnectData, X, cochainComplex, d, d₀, homologyIsoNeg, homologyIsoPos, map, restrictionGEIso, restrictionLEIso	10
Theorems X_negOne, X_negSucc, X_ofNat, X_zero, cochainComplex_X, cochainComplex_d, comp_d₀, comp_d₀_assoc, d_comp_d, d_comp_d_assoc, d_negSucc, d_ofNat, d_sub_one_zero, d_sub_two_sub_one, d_zero_one, d₀_comp, d₀_comp_assoc, homologyMap_map_of_eq_neg_succ, homologyMap_map_of_eq_succ, map_comp_map, map_f, map_id, restrictionGEIso_hom_f, restrictionGEIso_inv_f, restrictionLEIso_hom_f, restrictionLEIso_inv_f, shape	27
Total	37

CochainComplex

Definitions

Name	Category	Theorems
ConnectData 📖	CompData	—

CochainComplex.ConnectData

Definitions

Name	Category	Theorems
X 📖	CompOp	12 math math: cochainComplex_X, d_comp_d, restrictionLEIso_inv_f, X_zero, X_ofNat, restrictionLEIso_hom_f, d_comp_d_assoc, X_negOne, X_negSucc, restrictionGEIso_inv_f, shape, restrictionGEIso_hom_f
cochainComplex 📖	CompOp	11 math math: map_comp_map, cochainComplex_X, map_f, restrictionLEIso_inv_f, cochainComplex_d, restrictionLEIso_hom_f, restrictionGEIso_inv_f, map_id, homologyMap_map_of_eq_succ, homologyMap_map_of_eq_neg_succ, restrictionGEIso_hom_f
d 📖	CompOp	9 math math: d_ofNat, d_zero_one, d_comp_d, d_negSucc, d_sub_two_sub_one, cochainComplex_d, d_comp_d_assoc, shape, d_sub_one_zero
d₀ 📖	CompOp	5 math math: d₀_comp, d₀_comp_assoc, comp_d₀, comp_d₀_assoc, d_sub_one_zero
homologyIsoNeg 📖	CompOp	1 math math: homologyMap_map_of_eq_neg_succ
homologyIsoPos 📖	CompOp	1 math math: homologyMap_map_of_eq_succ
map 📖	CompOp	5 math math: map_comp_map, map_f, map_id, homologyMap_map_of_eq_succ, homologyMap_map_of_eq_neg_succ
restrictionGEIso 📖	CompOp	2 math math: restrictionGEIso_inv_f, restrictionGEIso_hom_f
restrictionLEIso 📖	CompOp	2 math math: restrictionLEIso_inv_f, restrictionLEIso_hom_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_negOne 📖	mathematical	—	X HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	—
X_negSucc 📖	mathematical	—	X HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	—
X_ofNat 📖	mathematical	—	X HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	—
X_zero 📖	mathematical	—	X HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	—
cochainComplex_X 📖	mathematical	—	HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex X	—	AddRightCancelSemigroup.toIsRightCancelAdd
cochainComplex_d 📖	mathematical	—	HomologicalComplex.d ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex d	—	AddRightCancelSemigroup.toIsRightCancelAdd
comp_d₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ComplexShape.up HomologicalComplex.d d₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
comp_d₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.d ComplexShape.up d₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_d₀
d_comp_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.d_comp_d Nat.instAtLeastTwoHAddOfNat Nat.cast_add Nat.cast_one d₀_comp comp_d₀ d_negSucc shape CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
d_comp_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_comp_d
d_negSucc 📖	mathematical	—	d HomologicalComplex.d ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
d_ofNat 📖	mathematical	—	d HomologicalComplex.d ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	—
d_sub_one_zero 📖	mathematical	—	d d₀	—	—
d_sub_two_sub_one 📖	mathematical	—	d HomologicalComplex.d ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	—
d_zero_one 📖	mathematical	—	d HomologicalComplex.d ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	—
d₀_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ComplexShape.up d₀ HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
d₀_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ComplexShape.up d₀ HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d₀_comp
homologyMap_map_of_eq_neg_succ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ComplexShape.up HomologicalComplex.Hom.f d₀	HomologicalComplex.homologyMap AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex map HomologicalComplex.homology CategoryTheory.Iso.hom homologyIsoNeg CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.cancel_mono HomologicalComplex.instMonoHomologyι HomologicalComplex.homologyι_naturality CategoryTheory.Category.assoc HomologicalComplex.restrictionHomologyIso_hom_homologyι HomologicalComplex.homologyι_naturality_assoc HomologicalComplex.restrictionHomologyIso_inv_homologyι_assoc CategoryTheory.cancel_epi HomologicalComplex.instEpiPOpcycles HomologicalComplex.p_opcyclesMap HomologicalComplex.pOpcycles_restrictionOpcyclesIso_inv_assoc HomologicalComplex.p_opcyclesMap_assoc HomologicalComplex.pOpcycles_restrictionOpcyclesIso_hom CategoryTheory.Iso.inv_hom_id_assoc
homologyMap_map_of_eq_succ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ComplexShape.up HomologicalComplex.Hom.f d₀	HomologicalComplex.homologyMap AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex map HomologicalComplex.homology CategoryTheory.Iso.hom homologyIsoPos CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.cancel_mono HomologicalComplex.instMonoHomologyι HomologicalComplex.homologyι_naturality CategoryTheory.Category.assoc HomologicalComplex.restrictionHomologyIso_hom_homologyι HomologicalComplex.homologyι_naturality_assoc HomologicalComplex.restrictionHomologyIso_inv_homologyι_assoc CategoryTheory.cancel_epi HomologicalComplex.instEpiPOpcycles HomologicalComplex.p_opcyclesMap HomologicalComplex.pOpcycles_restrictionOpcyclesIso_inv_assoc HomologicalComplex.p_opcyclesMap_assoc HomologicalComplex.pOpcycles_restrictionOpcyclesIso_hom CategoryTheory.Iso.inv_hom_id_assoc
map_comp_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ComplexShape.up HomologicalComplex.Hom.f d₀	CochainComplex AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory cochainComplex map ChainComplex	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext
map_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ComplexShape.up HomologicalComplex.Hom.f d₀	AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	—	AddRightCancelSemigroup.toIsRightCancelAdd
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id ChainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex ComplexShape.up AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex	—	HomologicalComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd
restrictionGEIso_hom_f 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.up Nat.instOne HomologicalComplex.restriction AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex ComplexShape.embeddingUpIntGE CategoryTheory.Iso.hom HomologicalComplex AddRightCancelSemigroup.toIsRightCancelAdd AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid HomologicalComplex.instCategory ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE restrictionGEIso X HomologicalComplex.X HomologicalComplex.restrictionXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE
restrictionGEIso_inv_f 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.up Nat.instOne HomologicalComplex.restriction AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex ComplexShape.embeddingUpIntGE CategoryTheory.Iso.inv HomologicalComplex AddRightCancelSemigroup.toIsRightCancelAdd AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid HomologicalComplex.instCategory ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE restrictionGEIso X HomologicalComplex.X HomologicalComplex.restrictionXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE
restrictionLEIso_hom_f 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.down Nat.instOne HomologicalComplex.restriction ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex ComplexShape.embeddingUpIntLE CategoryTheory.Iso.hom HomologicalComplex AddRightCancelSemigroup.toIsRightCancelAdd AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid HomologicalComplex.instCategory ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE restrictionLEIso X HomologicalComplex.X HomologicalComplex.restrictionXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE
restrictionLEIso_inv_f 📖	mathematical	—	HomologicalComplex.Hom.f ComplexShape.down Nat.instOne HomologicalComplex.restriction ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing cochainComplex ComplexShape.embeddingUpIntLE CategoryTheory.Iso.inv HomologicalComplex AddRightCancelSemigroup.toIsRightCancelAdd AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid HomologicalComplex.instCategory ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE restrictionLEIso X HomologicalComplex.X HomologicalComplex.restrictionXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE
shape 📖	mathematical	—	d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.shape AddRightCancelSemigroup.toIsRightCancelAdd d_negSucc neg_add_cancel Nat.cast_zero

---

← Back to Index