Mathlib Map

Theorems · Definition · category theory

SSet.Subcomplex.prodIso

{X Y : SSet} →
  (A : X.Subcomplex) →
    (B : Y.Subcomplex) → (A.prod B).toSSet ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj A.toSSet B.toSSet

The isomorphism (A.prod B).toSSet ≅ A.toSSet ⊗ B.toSSet.

Defined in
Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Cited by
3 results in Mathlib
Foundations
Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SSet.Subcomplex.unionProd.isPushout · cited by 2unionProd.isPushoutSSet.Subcomplex.prodIso_hom · cited by 0Subcomplex.prodIso_homSSet.Subcomplex.prodIso_inv · cited by 0Subcomplex.prodIso_invCategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compOpposite · cited by 8081OppositeCategoryTheory.Iso · cited by 3963CategoryTheory.IsoCategoryTheory.MonoidalCategoryStruct.tensorObj · cited by 3106MonoidalCategoryStruct.te…SimplexCategory · cited by 2204SimplexCategorySSet · cited by 1283SSetCategoryTheory.MonoidalCategoryStruct.tensorHom · cited by 587MonoidalCategoryStruct.te…SSet.Subcomplex · cited by 461SSet.SubcomplexSSet.Subcomplex.toSSet · cited by 315Subcomplex.toSSetCategoryTheory.SemiCartesianMonoidalCategory.fst · cited by 184SemiCartesianMonoidalCate…CategoryTheory.SemiCartesianMonoidalCategory.snd · cited by 181SemiCartesianMonoidalCate…CategoryTheory.CartesianMonoidalCategory.lift · cited by 160CartesianMonoidalCategory…SSet.Subcomplex.ι · cited by 136Subcomplex.ιSSet.Subcomplex.prod · cited by 13Subcomplex.prodSSet.Subcomplex.lift · cited by 12Subcomplex.liftSubcomplex.prodIsoCITED BYCITES

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by3

Results whose statement or proof uses this declaration.