simplicialCosimplicialAugmentedEquiv

Lean4

/-- The contravariant categorical equivalence between augmented simplicial
objects and augmented cosimplicial objects in the opposite category. -/
@[simps! functor inverse]
def simplicialCosimplicialAugmentedEquiv : (SimplicialObject.Augmented C)ᵒᵖ ≌ CosimplicialObject.Augmented Cᵒᵖ
    where
  functor := simplicialToCosimplicialAugmented _
  inverse := cosimplicialToSimplicialAugmented _
  unitIso :=
    NatIso.ofComponents (fun X => X.unop.rightOpLeftOpIso.op) fun f =>
      by
      dsimp
      rw [← f.op_unop]
      simp_rw [← op_comp]
      congr 1
      cat_disch
  counitIso := NatIso.ofComponents fun X => X.leftOpRightOpIso

Похожие утверждения