extendToSucc — Mathlib

English

There is a natural iso between restrictionLE of extendToSucc and F.

Русский

Существуют естественные изоморфизмы между restrictionLE extendToSucc и F.

LaTeX

$$$\\text{extendToSuccRestrictionLEIso} : \\text{SmallObject.restrictionLE} (extendToSucc\\; hj\\; F\\; τ) \\; (Order.le_succ j) \\cong F$$$

Lean4

/-- The extension to `Set.Iic (Order.succ j) ⥤ C` of a functor `F : Set.Iic j ⥤ C`,
when we specify a morphism `F.obj ⟨j, _⟩ ⟶ X`. -/
def extendToSucc : Set.Iic (Order.succ j) ⥤ C where
  obj := obj F X
  map {i₁ i₂} f := map hj F τ i₁ i₂ (leOfHom f) i₂.2
  map_id _ := extendToSucc.map_id _ F τ _ _
  map_comp {i₁ i₂ i₃} f g := extendToSucc.map_comp hj F τ i₁ i₂ i₃ (leOfHom f) (leOfHom g) i₃.2

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