English
Let F1, F2, F3 be presheaves and f1: F1 → F2, f2: F2 → F3 with f3: F1 → F3 and f1 ≫ f2 = f3. If f3 is locally surjective and f2 is locally injective, then f1 is locally surjective.
Русский
Пусть F1, F2, F3 — прешафы и f1: F1 → F2, f2: F2 → F3, с f3: F1 → F3 и равенство f1 ≫ f2 = f3. Если f3 локально сюръективен, а f2 локально инъективен, то f1 локально сюръективен.
LaTeX
$$Eq (f1 ≫ f2) f3 → IsLocallySurjective_J(f3) → IsLocallyInjective_J(f2) → IsLocallySurjective_J(f1)$$
Lean4
theorem isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} {f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃} (f₃ : F₁ ⟶ F₃) (fac : f₁ ≫ f₂ = f₃) [IsLocallyInjective J f₃] [IsLocallySurjective J f₁] :
IsLocallyInjective J f₂ := by
subst fac
exact isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective J f₁ f₂
