arrowMap — Mathlib

English

Given a linear order J and a functor F: Set.Iic j ⥤ C, arrowMap returns the Arrow C corresponding to the image under F of the inequality between i1 and i2.

Русский

Для линейного порядка J и функторa F: Set.Iic j ⥤ C, arrowMap возвращает стрелу C, образованную F по неравенству i1 ≤ i2.

LaTeX

$$arrowMap {j : J} (F : Set.Iic j ⥤ C) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j) : Arrow C$$

Lean4

/-- Given a functor `F : Set.Iic ⥤ C`, this is the morphism in `C`, as an element
in `Arrow C`, that is obtained by applying `F.map` to an inequality. -/
def arrowMap {j : J} (F : Set.Iic j ⥤ C) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j) : Arrow C :=
  Arrow.mk (F.map (homOfLE h₁₂ : ⟨i₁, h₁₂.trans h₂⟩ ⟶ ⟨i₂, h₂⟩))

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