isLocallySurjective_of_iso — Mathlib

English

If F is locally surjective as a Presheaf, then the induced map in Sheaf is locally surjective.

Русский

Если F является локально сюрьективным прешейфом, то соответствующее отображение в Sheaf локально сюрьективно.

LaTeX

$$$\text{IsLocallySurjective}_J(f) \Rightarrow \text{IsLocallySurjective}_{J}^{\text{Sheaf}}(f)$$$

Lean4

instance isLocallySurjective_of_iso [IsIso φ] : IsLocallySurjective φ :=
  by
  have : IsIso φ.val := (inferInstance : IsIso ((sheafToPresheaf J A).map φ))
  infer_instance

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