isLocallySurjective_of_isLocallySurjective

English

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

Русский

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

LaTeX

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

Lean4

theorem isLocallySurjective_of_isLocallySurjective {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃)
    [IsLocallySurjective J (f₁ ≫ f₂)] : IsLocallySurjective J f₂ where
  imageSieve_mem {X}
    x := by
    refine J.superset_covering ?_ (imageSieve_mem J (f₁ ≫ f₂) x)
    intro Y g hg
    exact ⟨f₁.app _ (localPreimage (f₁ ≫ f₂) x g hg), by simpa using app_localPreimage (f₁ ≫ f₂) x g hg⟩

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