evalCompCoyonedaCorepresentableByDoubleId

English

If i has no successors with respect to the complex shape c (i.e., c.Rel i j is false for all j), then for any C, the evaluation functor at i against X is corepresented by the object (single C c i).obj X.

Русский

Если у индекса i нет successor по форме комплекса, то для любого C функция-оценка в i относительно X представляется единичным объектом (single C c i).obj X.

LaTeX

$$$\forall i, \big( \forall j, ¬ c.Rel i j \big) \to ((eval C c i) \circ (Coyoneda.obj (op X))).CorepresentableBy ((single C c i).obj X)$$$

Lean4

/-- Let `c : ComplexShape ι`, and `i₀` and `i₁` be distinct indices such
that `hi₀₁ : c.Rel i₀ i₁`, then for any `X : C`, the functor which sends
`K : HomologicalComplex C c` to `X ⟶ K.X i` is corepresentable by `double (𝟙 X) hi₀₁`. -/
@[simps -isSimp]
noncomputable def evalCompCoyonedaCorepresentableByDoubleId (h : i₀ ≠ i₁) (X : C) :
    (eval C c i₀ ⋙ coyoneda.obj (op X)).CorepresentableBy (double (𝟙 X) hi₀₁)
    where
  homEquiv
    {K} :=
    { toFun g := (doubleXIso₀ _ hi₀₁).inv ≫ g.f i₀
      invFun φ₀ := mkHomFromDouble _ h φ₀ (φ₀ ≫ K.d i₀ i₁) (by simp) (by simp)
      left_inv
        g := by
        ext
        · simp
        · simp [double_d _ _ h]
      right_inv _ := by simp }
  homEquiv_comp _ _ := by simp

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