inductiveSystem — Mathlib

English

When j is a limit element, the inductive construction yields an object in Φ.Iteration j built from the system of objects Φ.Iteration i for i<j via the functor on the inductive system.

Русский

При предельном элементе j индуктивная конструкция даёт объект в Φ.Iteration j, построенный из системы объектов Φ.Iteration i для i<j через функтор индуктивной системы.

LaTeX

$$$\\mathrm{InductiveSystem} \\to Φ.Iteration j$ via functor on limits$$

Lean4

/-- Assuming `j : J` is a limit element and that we have `∀ (i : J), i < j → Φ.Iteration i`,
this is the inductive system `Set.Iio j ⥤ C` which sends `⟨i, _⟩` to
`(iter i _).F.obj ⟨i, _⟩`. -/
@[simps]
noncomputable def inductiveSystem : Set.Iio j ⥤ C
    where
  obj i := (iter i.1 i.2).F.obj ⟨i.1, by simp⟩
  map {i₁ i₂} f := mapObj (iter i₁.1 i₁.2) (iter i₂.1 i₂.2) (leOfHom f) (by simp) (by simp) (leOfHom f)

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