evalCompCoyonedaCorepresentableBySingle

English

For AreComplementary embeddings e1 and e2 into c, the function fromSum e1 e2 : Sum I1 I2 → I is bijective, establishing a bijection between the disjoint union of index sets and the total index set.

Русский

Для вложений e1, e2, образующих AreComplementary, отображение fromSum e1 e2: Sum I1 I2 → I реализует биекцию между объединением индексов и общим множеством индексов.

LaTeX

$$Let e1 : c1.Embedding c, e2 : c2.Embedding c with AreComplementary e1 e2. Then Function.Bijective (ComplexShape.Embedding.AreComplementary.fromSum e1 e2).$$

Lean4

/-- If `i` has no successor for the complex shape `c`,
then for any `X : C`, the functor which sends `K : HomologicalComplex C c`
to `X ⟶ K.X i` is corepresentable by `(single C c i).obj X`. -/
@[simps -isSimp]
noncomputable def evalCompCoyonedaCorepresentableBySingle (i : ι) [DecidableEq ι] (hi : ∀ (j : ι), ¬c.Rel i j) (X : C) :
    (eval C c i ⋙ coyoneda.obj (op X)).CorepresentableBy ((single C c i).obj X)
    where
  homEquiv
    {K} :=
    { toFun g := (singleObjXSelf c i X).inv ≫ g.f i
      invFun f := mkHomFromSingle f (fun j hj ↦ (hi j hj).elim)
      left_inv g := by cat_disch
      right_inv f := by simp }
  homEquiv_comp := by simp

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