RelativeMorphism

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/RelativeMorphism.lean

Statistics

Metric	Count
Definitions RelativeMorphism, h, ofEq, postcomp, precomp, refl, HomotopyClass, postcomp, precomp, comp, const, homotopyClass, map, ofSimplex₀	14
Theorems eq, ext, ext_iff, h₀, h₀_assoc, h₁, h₁_assoc, ofEq_h, postcomp_h, precomp_h, refl_h, rel, rel_assoc, eq_homotopyClass, comm, comm_assoc, comp_map, const_map, ext, ext_iff, image_le, le_preimage, map_coe, map_eq_of_mem, ofSimplex₀_map, postcomp_homotopyClass, precomp_homotopyClass	27
Total	41

SSet

Definitions

Name	Category	Theorems
RelativeMorphism 📖	CompData	—

SSet.RelativeMorphism

Definitions

Name	Category	Theorems
HomotopyClass 📖	CompOp	—
comp 📖	CompOp	5 math math: precomp_homotopyClass, postcomp_homotopyClass, Homotopy.precomp_h, Homotopy.postcomp_h, comp_map
const 📖	CompOp	1 math math: const_map
homotopyClass 📖	CompOp	4 math math: HomotopyClass.eq_homotopyClass, precomp_homotopyClass, postcomp_homotopyClass, Homotopy.eq
map 📖	CompOp	28 math math: image_le, Homotopy.h₀_assoc, ext_iff, SSet.PtSimplex.RelStruct.δ_castSucc_map, SSet.PtSimplex.RelStruct.δ_castSucc_map_assoc, SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc, ofSimplex₀_map, SSet.PtSimplex.MulStruct.δ_succ_succ_map, le_preimage, map_eq_of_mem, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map, comm_assoc, comm, Homotopy.h₁_assoc, Homotopy.ofEq_h, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map_assoc, Homotopy.h₀, Homotopy.precomp_h, Homotopy.h₁, Homotopy.postcomp_h, const_map, Homotopy.refl_h, SSet.PtSimplex.RelStruct.δ_succ_map, comp_map, map_coe, SSet.PtSimplex.MulStruct.δ_succ_castSucc_map_assoc, SSet.PtSimplex.RelStruct.δ_succ_map_assoc, SSet.PtSimplex.MulStruct.δ_castSucc_castSucc_map
ofSimplex₀ 📖	CompOp	1 math math: ofSimplex₀_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.Subcomplex.toSSet SSet.Subcomplex.ι map	—	—
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.Subcomplex.toSSet SSet.Subcomplex.ι map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
comp_map 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.Subcomplex.toSSet	map comp	—	—
const_map 📖	mathematical	—	map SSet.Subcomplex.ofSimplex const SSet.const	—	—
ext 📖	—	map	—	—	—
ext_iff 📖	mathematical	—	map	—	ext
image_le 📖	mathematical	—	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory SSet.Subcomplex.image map	—	map_coe
le_preimage 📖	mathematical	—	SSet.Subcomplex Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory SSet.Subcomplex.preimage map	—	image_le
map_coe 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types map CategoryTheory.Functor.obj Set Set.instMembership CategoryTheory.Subfunctor.obj SSet.Subcomplex.toSSet	—	map_eq_of_mem
map_eq_of_mem 📖	mathematical	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Set Set.instMembership CategoryTheory.Subfunctor.obj	CategoryTheory.NatTrans.app map SSet.Subcomplex.toSSet	—	CategoryTheory.congr_app comm
ofSimplex₀_map 📖	mathematical	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types Opposite.op	map SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet CategoryTheory.Functor.obj Set Set.instMembership CategoryTheory.Subfunctor.obj SSet.Subcomplex.mem_ofSimplex_obj ofSimplex₀	—	SSet.Subcomplex.mem_ofSimplex_obj
postcomp_homotopyClass 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.Subcomplex.toSSet	HomotopyClass.postcomp homotopyClass comp	—	—
precomp_homotopyClass 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.Subcomplex.toSSet	HomotopyClass.precomp homotopyClass comp	—	—

SSet.RelativeMorphism.Homotopy

Definitions

Name	Category	Theorems
h 📖	CompOp	11 math math: h₀_assoc, ext_iff, h₁_assoc, ofEq_h, h₀, precomp_h, h₁, postcomp_h, rel, refl_h, rel_assoc
ofEq 📖	CompOp	1 math math: ofEq_h
postcomp 📖	CompOp	1 math math: postcomp_h
precomp 📖	CompOp	1 math math: precomp_h
refl 📖	CompOp	1 math math: refl_h

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	—	SSet.RelativeMorphism.homotopyClass	—	—
ext 📖	—	h	—	—	—
ext_iff 📖	mathematical	—	h	—	ext
h₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.ι₀ h SSet.RelativeMorphism.map	—	—
h₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.ι₀ h SSet.RelativeMorphism.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h₀
h₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.ι₁ h SSet.RelativeMorphism.map	—	—
h₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.ι₁ h SSet.RelativeMorphism.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h₁
ofEq_h 📖	mathematical	—	h ofEq CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.SemiCartesianMonoidalCategory.fst SSet.RelativeMorphism.map	—	—
postcomp_h 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.Subcomplex.toSSet	h SSet.RelativeMorphism.comp postcomp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex SSet.RelativeMorphism.map	—	—
precomp_h 📖	mathematical	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory SSet.Subcomplex.toSSet	h SSet.RelativeMorphism.comp precomp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.MonoidalCategoryStruct.whiskerRight SSet.RelativeMorphism.map	—	—
refl_h 📖	mathematical	—	h refl CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.SemiCartesianMonoidalCategory.fst SSet.RelativeMorphism.map	—	—
rel 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory SSet.Subcomplex.toSSet CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.MonoidalCategoryStruct.whiskerRight SSet.Subcomplex.ι h CategoryTheory.SemiCartesianMonoidalCategory.fst	—	—
rel_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory SSet.instCartesianMonoidalCategory SSet.Subcomplex.toSSet CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.MonoidalCategoryStruct.whiskerRight SSet.Subcomplex.ι h CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rel

SSet.RelativeMorphism.HomotopyClass

Definitions

Name	Category	Theorems
postcomp 📖	CompOp	1 math math: SSet.RelativeMorphism.postcomp_homotopyClass
precomp 📖	CompOp	1 math math: SSet.RelativeMorphism.precomp_homotopyClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_homotopyClass 📖	mathematical	—	SSet.RelativeMorphism.homotopyClass	—	Quot.mk_surjective

---

← Back to Index