Theorems · Definition · category theory

SSet.Truncated.liftOfStrictSegal.naturalityProperty

{X Y : SSet.Truncated 2} →
  (f₀ :
      X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
        Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })) →
    (f₁ :
        X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
          Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })) →
      (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
          f₀
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
                x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
              (f₁ x)) →
        (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
            f₀
                ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                  x) =
              (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                (f₁ x)) →
          Y.StrictSegal → CategoryTheory.MorphismProperty (SimplexCategory.Truncated 2)

The property of morphisms in SimplexCategory.Truncated 2 for which liftOfStrictSegal.app is natural.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound