instIsLocallySurjectiveHomObjForgetTypeWhiskerRightOpposite

English

If f is locally surjective with respect to J, then the whiskered morphism whiskerRight f (forget A) is also locally surjective with respect to J.

Русский

Если f локально сюрьективен относительно J, то отображение, полученное остаточным растяжением f через forget A, тоже локально сюрьективно.

LaTeX

$$$\text{IsLocallySurjective}_J(f) \Rightarrow \text{IsLocallySurjective}_J(\mathrm{whiskerRight}(f, \mathrm{forget}\ A))$$$

Lean4

instance {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) [IsLocallySurjective J f] : IsLocallySurjective J (whiskerRight f (forget A)) where
  imageSieve_mem s := imageSieve_mem J f s

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