functorPushforward_imageSieve_mem

English

If G is locally full with respect to K, then for any U,V and morphism f: G.obj U → G.obj V, the pushforward of the image sieve along G lies in K.

Русский

Если G локально полно относительно K, то образная сива (pushforward) образа f вдоль G принадлежит K.

LaTeX

$$$(G.imageSieve f).functorPushforward G \in K _$$$

Lean4

theorem functorPushforward_imageSieve_mem [G.IsLocallyFull K] {U V} (f : G.obj U ⟶ G.obj V) :
    (G.imageSieve f).functorPushforward G ∈ K _ :=
  Functor.IsLocallyFull.functorPushforward_imageSieve_mem _

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