of_underPost — Mathlib

English

If F is essentially surjective, then the under-post construction preserves essential surjectivity of F.

Русский

Если F существенно сюръектен, под конструкция Under.post сохраняет essSurj F.

LaTeX

$$$\mathsf{EssSurj}\big(\mathrm{toUnder}(X,F)\big)$$$

Lean4

theorem of_underPost {Y : Under (F.obj X)} : (Under.post F (X := X)).essImage Y → F.essImage Y.right := fun ⟨Z, ⟨e⟩⟩ ↦
  ⟨Z.right, ⟨(Under.forget _).mapIso e⟩⟩

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