English
If φ is a covering prefunctor and the composite φ ⋙q ψ is covering and φ.obj is surjective, then ψ is a covering prefunctor.
Русский
Если φ — покрывающий префунктор, композиция φ ⋙q ψ покрывающая и φ.obj сюръективна, тогда ψ — покрывающий префунктор.
LaTeX
$$\operatorname{IsCovering}(\phi) \land \operatorname{IsCovering}(\phi \circ \psi) \land \operatorname{Surjective}(\phi.obj) \Rightarrow \operatorname{IsCovering}(\psi)$$
Lean4
theorem of_comp_left (hφ : φ.IsCovering) (hφψ : (φ ⋙q ψ).IsCovering) (φsur : Surjective φ.obj) : ψ.IsCovering :=
by
refine ⟨fun v => ?_, fun v => ?_⟩ <;> obtain ⟨u, rfl⟩ := φsur v
exacts [(Bijective.of_comp_iff _ (hφ.star_bijective u)).mp (hφψ.star_bijective u),
(Bijective.of_comp_iff _ (hφ.costar_bijective u)).mp (hφψ.costar_bijective u)]
