isLocallySurjective_comp_iff — Mathlib

English

Let F1, F2, F3 be presheaves with f3 = f1 ≫ f2. If f3 is locally surjective and f2 is locally injective, then f1 is locally surjective.

Русский

Пусть F1, F2, F3 — прешафы, f3 = f1 ≫ f2; если f3 локально сюръективен и f2 локально инъективен, то f1 локально сюрективен.

LaTeX

$$Eq (f1 ≫ f2) f3 → IsLocallySurjective_J(f3) → IsLocallyInjective_J(f2) → IsLocallySurjective_J(f1)$$

Lean4

theorem isLocallySurjective_comp_iff {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃) [IsLocallyInjective J f₂]
    [IsLocallySurjective J f₂] : IsLocallySurjective J (f₁ ≫ f₂) ↔ IsLocallySurjective J f₁ :=
  by
  constructor
  · intro
    exact isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective J f₁ f₂
  · intro
    infer_instance

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