isLocallySurjective_of_isLocallySurjective_fac

English

If f1 ≫ f2 = f3 and f1 is locally surjective, then f3 is locally surjective iff f2 is locally surjective.

Русский

Если f1 ≫ f2 = f3 и f1 локально сюрьективен, тогда f3 локально сюрективен тогда и только тогда, когда f2 локально сюрективен.

LaTeX

$$$\text{fac}: f_1 \circ f_2 = f_3,\ \text{IsLocallySurjective}_J(f_1) \Rightarrow \big( \text{IsLocallySurjective}_J(f_3) \iff \text{IsLocallySurjective}_J(f_2) \big)$$$

Lean4

theorem isLocallySurjective_of_isLocallySurjective_fac {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} {f₁ : F₁ ⟶ F₂} {f₂ : F₂ ⟶ F₃} {f₃ : F₁ ⟶ F₃}
    (fac : f₁ ≫ f₂ = f₃) [IsLocallySurjective J f₃] : IsLocallySurjective J f₂ :=
  by
  subst fac
  exact isLocallySurjective_of_isLocallySurjective J f₁ f₂

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