instIsLocallySurjectiveHomObjForgetTypeToImage

English

If f is locally surjective, then its image in a Sheaf of Type w is locally surjective.

Русский

Если f локально сюрьективен, то его образ в Sheaf типа w локально сюрьективен.

LaTeX

$$$\text{IsLocallySurjective}_J(f) \Rightarrow \text{IsLocallySurjective}_J(\mathrm{image}(f))$$$

Lean4

instance {F G : Sheaf J (Type w)} (f : F ⟶ G) : IsLocallySurjective (Sheaf.toImage f) :=
  by
  dsimp [Sheaf.toImage]
  infer_instance

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