isLocallySurjective_iff_of_fac — Mathlib

English

For f1, f2, f3 with fac, the local surjectivity of f1 implies the equivalence between f3 and f2 in local surjectivity.

Русский

Для f1, f2, f3 с(face) fac локальная сюрьективность f1 порождает эквивалентность между f3 и f2 по локальной сюрьективности.

LaTeX

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

Lean4

theorem isLocallySurjective_iff_of_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₃ ↔ IsLocallySurjective J f₂ :=
  by
  constructor
  · intro
    exact isLocallySurjective_of_isLocallySurjective_fac J fac
  · intro
    rw [← fac]
    infer_instance

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