Commit 2025-12-26 18:30 41b24eaf

View on Github →

feat(AlgebraicTopology): prerequisites for the commutation of HomotopyCategory with binary products (#33201)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/CompStructTruncated.lean

added def SSet.Truncated.Edge.CompStruct.idCompId

Created Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean

added def SSet.Truncated.Edge.CompStruct.tensor

added theorem SSet.Truncated.Edge.id_tensor_id

added theorem SSet.Truncated.Edge.map_associator_hom

added theorem SSet.Truncated.Edge.map_fst

added theorem SSet.Truncated.Edge.map_snd

added theorem SSet.Truncated.Edge.map_tensorHom

added theorem SSet.Truncated.Edge.map_whiskerLeft

added theorem SSet.Truncated.Edge.map_whiskerRight

added def SSet.Truncated.Edge.tensor

added theorem SSet.Truncated.Edge.tensor_surjective

added def SSet.Truncated.HomotopyCategory.isoTerminal

added theorem SSet.Truncated.HomotopyCategory.square

Modified Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

added theorem SSet.Truncated.HomotopyCategory.ext

added def SSet.Truncated.HomotopyCategory.isTerminal

Modified Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

added theorem SSet.Truncated.tensor_map_apply_fst

added theorem SSet.Truncated.tensor_map_apply_snd

Modified Mathlib/CategoryTheory/Category/ReflQuiv.lean

Modified Mathlib/CategoryTheory/Functor/Currying.lean

added def CategoryTheory.Functor.fullyFaithfulCurry

Modified Mathlib/CategoryTheory/Functor/CurryingThree.lean

added def CategoryTheory.Functor.fullyFaithfulCurry₃

Modified Mathlib/CategoryTheory/Products/Basic.lean

added theorem CategoryTheory.prod_id'