functorToMonoOver — Mathlib

English

There is a functor from J to MonoOver X given by transfinite iterations with Lebesgue-like limits.

Русский

Существует функтор из J в MonoOver X, заданный трансфинитной итерацией с пределами.

LaTeX

$$$\text{functorToMonoOver } hG A0 : J \to MonoOver X$$$

Lean4

/-- Let `C` be a Grothendieck abelian category with a generator (`hG`),
`X : C`, `A₀ : Subobject X`. Let `J` be a well-ordered type. This is
the functor `J ⥤ MonoOver X` which corresponds to the evaluation
at `A₀` of the transfinite iteration of the map
`largerSubobject hG : Subobject X → Subobject X`. -/
@[simps]
noncomputable def functorToMonoOver : J ⥤ MonoOver X
    where
  obj j := MonoOver.mk' (transfiniteIterate (largerSubobject hG) j A₀).arrow
  map {j j'}
    f := MonoOver.homMk (Subobject.ofLE _ _ (monotone_transfiniteIterate _ _ (le_largerSubobject hG) (leOfHom f)))

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