Homotopy

📁 Source: Mathlib/CategoryTheory/Sites/Hypercover/Homotopy.lean

Statistics

Metric	Count
Definitions HOneHypercover, cylinder, homotopicRel, toHOneHypercover, Homotopy, H, a, cylinder, cylinderHom, cylinderHomotopy, cylinderX, cylinderf, Homotopy, Homotopy, Homotopy, Homotopy, Homotopy	17
Theorems instNonempty, isCofiltered_of_hasPullbacks, cylinder_toPreOneHypercover, exists_nonempty_homotopy, mapMultiforkOfIsLimit_eq, map_eq_map, wl, wl_assoc, wr, wr_assoc, cylinderHom_h₀, cylinderHom_h₁, cylinderHom_s₀, cylinderHom_s₁, cylinder_I₀, cylinder_I₁, cylinder_X, cylinder_Y, cylinder_f, cylinder_p₁, cylinder_p₂, exists_nonempty_homotopy, sieve₀_cylinder, sieve₁'_cylinder, toPullback_cylinder	25
Total	42

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
HOneHypercover 📖	CompOp	3 math math: HOneHypercover.instNonempty, CategoryTheory.PreOneHypercover.Homotopy.map_eq_map, HOneHypercover.isCofiltered_of_hasPullbacks

CategoryTheory.GrothendieckTopology.HOneHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonempty 📖	mathematical	—	CategoryTheory.GrothendieckTopology.HOneHypercover	—	CategoryTheory.GrothendieckTopology.OneHypercover.instNonempty
isCofiltered_of_hasPullbacks 📖	mathematical	—	CategoryTheory.IsCofiltered CategoryTheory.GrothendieckTopology.HOneHypercover CategoryTheory.Quotient.category CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.GrothendieckTopology.OneHypercover.instCategory CategoryTheory.GrothendieckTopology.OneHypercover.homotopicRel	—	CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Presieve.instHasPullbacksOfHasPullbacks CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Functor.map_surjective CategoryTheory.Quotient.full_functor CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy CategoryTheory.Functor.map_comp CategoryTheory.PreOneHypercover.Homotopy.map_eq_map instNonempty

CategoryTheory.GrothendieckTopology.OneHypercover

Definitions

Name	Category	Theorems
cylinder 📖	CompOp	1 math math: cylinder_toPreOneHypercover
homotopicRel 📖	CompOp	2 math math: CategoryTheory.PreOneHypercover.Homotopy.map_eq_map, CategoryTheory.GrothendieckTopology.HOneHypercover.isCofiltered_of_hasPullbacks
toHOneHypercover 📖	CompOp	1 math math: CategoryTheory.PreOneHypercover.Homotopy.map_eq_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cylinder_toPreOneHypercover 📖	mathematical	—	toPreOneHypercover cylinder CategoryTheory.PreOneHypercover.cylinder	—	—
exists_nonempty_homotopy 📖	mathematical	—	CategoryTheory.PreOneHypercover.Homotopy toPreOneHypercover CategoryTheory.PreOneHypercover.Hom.comp	—	—

CategoryTheory.PreOneHypercover

Definitions

Name	Category	Theorems
Homotopy 📖	CompData	2 math math: CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy, exists_nonempty_homotopy
cylinder 📖	CompOp	15 math math: cylinder_X, cylinderHom_h₁, cylinder_I₀, cylinder_f, cylinder_I₁, sieve₀_cylinder, sieve₁'_cylinder, toPullback_cylinder, CategoryTheory.GrothendieckTopology.OneHypercover.cylinder_toPreOneHypercover, cylinder_p₁, cylinder_p₂, cylinderHom_s₁, cylinderHom_s₀, cylinderHom_h₀, cylinder_Y
cylinderHom 📖	CompOp	4 math math: cylinderHom_h₁, cylinderHom_s₁, cylinderHom_s₀, cylinderHom_h₀
cylinderHomotopy 📖	CompOp	—
cylinderX 📖	CompOp	6 math math: cylinder_X, cylinderHom_h₁, toPullback_cylinder, cylinder_p₁, cylinder_p₂, cylinder_Y
cylinderf 📖	CompOp	6 math math: cylinderHom_h₁, cylinder_f, toPullback_cylinder, cylinder_p₁, cylinder_p₂, cylinder_Y

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cylinderHom_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ toPreZeroHypercover cylinder Hom.toHom cylinderHom CategoryTheory.Limits.pullback.fst CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.I₀ I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Y CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.lift toPullback	—	—
cylinderHom_h₁ 📖	mathematical	—	Hom.h₁ cylinder cylinderHom CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback cylinderX CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom cylinderf Y CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.lift CategoryTheory.PreZeroHypercover.Hom.h₀ toPullback CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct p₁ p₂	—	—
cylinderHom_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover cylinder Hom.toHom cylinderHom CategoryTheory.PreZeroHypercover.I₀ I₁	—	—
cylinderHom_s₁ 📖	mathematical	—	Hom.s₁ cylinder cylinderHom I₁ CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom	—	—
cylinder_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover cylinder I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom	—	—
cylinder_I₁ 📖	mathematical	—	I₁ cylinder CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom	—	—
cylinder_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X toPreZeroHypercover cylinder cylinderX CategoryTheory.PreZeroHypercover.I₀ I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom	—	—
cylinder_Y 📖	mathematical	—	Y cylinder CategoryTheory.Limits.pullback cylinderX CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom cylinderf CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.lift CategoryTheory.PreZeroHypercover.Hom.h₀ toPullback CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct p₁ p₂	—	—
cylinder_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f toPreZeroHypercover cylinder cylinderf CategoryTheory.PreZeroHypercover.I₀ I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom	—	—
cylinder_p₁ 📖	mathematical	—	p₁ cylinder CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback cylinderX CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom cylinderf Y CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.lift CategoryTheory.PreZeroHypercover.Hom.h₀ toPullback CategoryTheory.CategoryStruct.id p₂	—	—
cylinder_p₂ 📖	mathematical	—	p₂ cylinder CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback cylinderX CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom cylinderf Y CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.lift CategoryTheory.PreZeroHypercover.Hom.h₀ toPullback CategoryTheory.CategoryStruct.id p₁ CategoryTheory.Limits.pullback.snd	—	—
exists_nonempty_homotopy 📖	mathematical	—	Homotopy Hom.comp	—	—
sieve₀_cylinder 📖	mathematical	—	CategoryTheory.PreZeroHypercover.sieve₀ toPreZeroHypercover cylinder CategoryTheory.Sieve.generate CategoryTheory.Presieve.bindOfArrows CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.Sieve.arrows CategoryTheory.Sieve.pullback CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks CategoryTheory.Presieve.ofArrows CategoryTheory.Limits.pullback.lift CategoryTheory.PreZeroHypercover.Hom.h₀ sieve₁'	—	le_antisymm CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks CategoryTheory.PreZeroHypercover.sieve₀.eq_1 CategoryTheory.Sieve.generate_le_iff CategoryTheory.Limits.pullback.condition CategoryTheory.Sieve.downward_closed CategoryTheory.Category.id_comp w CategoryTheory.Limits.limit.lift_π_assoc
sieve₁'_cylinder 📖	mathematical	—	sieve₁' cylinder CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks CategoryTheory.Presieve.ofArrows CategoryTheory.Sieve.pullback CategoryTheory.Limits.pullback I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom Y CategoryTheory.Limits.pullback.lift CategoryTheory.PreZeroHypercover.Hom.h₀ toPullback CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.fst CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	le_antisymm CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks sieve₁'.eq_1 CategoryTheory.Sieve.ofArrows.eq_1 CategoryTheory.Sieve.generate_le_iff toPullback_cylinder CategoryTheory.Limits.pullback.condition w CategoryTheory.Sieve.pullbackArrows_comm CategoryTheory.Presieve.hasPullback CategoryTheory.Limits.hasPullback_symmetry CategoryTheory.Sieve.downward_closed
toPullback_cylinder 📖	mathematical	—	toPullback cylinder CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks CategoryTheory.Presieve.ofArrows CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback cylinderX I₁ CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom cylinderf Y CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.lift CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct p₁ p₂	—	CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks w CategoryTheory.Limits.limit.lift_π

CategoryTheory.PreOneHypercover.Homotopy

Definitions

Name	Category	Theorems
H 📖	CompOp	4 math math: wl, wl_assoc, wr, wr_assoc
a 📖	CompOp	4 math math: wl, wl_assoc, wr, wr_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMultiforkOfIsLimit_eq 📖	mathematical	—	CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit	—	CategoryTheory.Limits.Multifork.IsLimit.hom_ext CategoryTheory.Limits.Multifork.condition CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι wl CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' wr
map_eq_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.GrothendieckTopology.OneHypercover.instCategory CategoryTheory.GrothendieckTopology.HOneHypercover CategoryTheory.Quotient.category CategoryTheory.GrothendieckTopology.OneHypercover.homotopicRel CategoryTheory.GrothendieckTopology.OneHypercover.toHOneHypercover	—	CategoryTheory.Quotient.sound
wl 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.Hom.toHom H a CategoryTheory.PreOneHypercover.p₁ CategoryTheory.PreZeroHypercover.Hom.h₀	—	—
wl_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.Hom.toHom H a CategoryTheory.PreOneHypercover.p₁ CategoryTheory.PreZeroHypercover.Hom.h₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' wl
wr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.Hom.toHom H a CategoryTheory.PreOneHypercover.p₂ CategoryTheory.PreZeroHypercover.Hom.h₀	—	—
wr_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.Hom.toHom H a CategoryTheory.PreOneHypercover.p₂ CategoryTheory.PreZeroHypercover.Hom.h₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' wr

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
Homotopy 📖	CompData	3 math math: Homotopy.equivSubZero_symm_apply, HomotopyEquiv.ext_iff, Homotopy.equivSubZero_apply

ContinuousMap

Definitions

Name	Category	Theorems
Homotopy 📖	CompData	27 math math: Homotopy.apply_zero_path, Homotopy.evalAt_eq, Homotopy.ulift_apply, Homotopy.cast_apply, Path.toHomotopyConst_apply, Homotopy.compContinuousMap_apply, Homotopy.comp_apply, Homotopy.symm_bijective, Homotopy.apply_one_path, Homotopy.instHomotopyLike, Homotopy.extend_apply_coe, Homotopy.evalAt_apply, Homotopy.symm_apply, Homotopy.trans_apply, Homotopy.curry_apply, Homotopy.extend_apply_of_mem_I, Homotopy.continuous, Homotopy.affine_apply, Homotopy.coe_toContinuousMap, Homotopy.apply_zero, Homotopy.prod_apply, Homotopy.apply_one, Homotopy.congr_fun, Homotopy.ext_iff, HomotopyWith.coe_toHomotopy, Homotopy.refl_apply, Homotopy.congr_arg

Path

Definitions

Name	Category	Theorems
Homotopy 📖	CompOp	10 math math: Homotopy.symm_bijective, Homotopy.map_apply, Homotopy.target, Homotopy.hcomp_half, Homotopy.hcomp_apply, Homotopy.trans_apply, Homotopy.coeFn_injective, Homotopy.source, Homotopy.symm₂_apply, isSimplyConnected_iff_exists_homotopy_refl_forall_mem

SSet.RelativeMorphism

Definitions

Name	Category	Theorems
Homotopy 📖	CompData	—

(root)

Definitions

Name	Category	Theorems
Homotopy 📖	CompData	12 math math: CochainComplex.IsKInjective.nonempty_homotopy_zero, HomotopyCategory.isZero_quotient_obj_iff, CochainComplex.IsKProjective.homotopyZero_def, CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId, HomotopyCategory.quotient_map_eq_zero_iff, HomologicalComplex.homotopyCofiber.descSigma_ext_iff, CochainComplex.IsKInjective.homotopyZero_def, CochainComplex.IsKProjective.nonempty_homotopy_zero, CochainComplex.HomComplex.Cochain.equivHomotopy_apply_of_eq, CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId, CochainComplex.HomComplex.Cochain.equivHomotopy_apply_coe, CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom

---

← Back to Index