English
If φ is covering and φ ⋙ ψ is covering, and φ.obj is surjective, then ψ is covering.
Русский
Если φ — покрывающий префунктор, φ ⋙ ψ — пок Default, и φ.obj сюръективна, тогда ψ — покрывающий префунктор.
LaTeX
$$\operatorname{IsCovering}(\phi) \land \operatorname{IsCovering}(\phi \circ \psi) \land \operatorname{Surjective}(\phi.obj) \Rightarrow \operatorname{IsCovering}(\psi)$$
Lean4
theorem symmetrifyStar (u : U) :
φ.symmetrify.star u = (Quiver.symmetrifyStar _).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ Quiver.symmetrifyStar u :=
by
rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyStar (φ.obj u))]
ext ⟨v, f | g⟩ <;>
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [Quiver.symmetrifyStar]`
simp only [Quiver.symmetrifyStar, Function.comp_apply] <;>
erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply] <;>
simp
