hasOfPrecompProperty_epimorphisms

English

If P is stable under cobase change, then P.HasOfPrecompProperty holds for the class of epimorphisms, meaning precomposition with epi preserves P in pushout configurations.

Русский

Если P устойчива к cobase change, то свойство HasOfPrecompProperty выполняется для эпиморфизмов: предкомпозиция с эпиморфизмом сохраняет P в конфигурациях пуш-аут.

LaTeX

$$$P.IsStableUnderCobaseChange \Rightarrow P.HasOfPrecompProperty(\text{MorphismProperty epimorphisms})$$$

Lean4

instance hasOfPrecompProperty_epimorphisms [P.IsStableUnderCobaseChange] :
    P.HasOfPrecompProperty (MorphismProperty.epimorphisms C) where
  of_precomp {X Y Z} f g (hf : Epi f)
    hcomp :=
    by
    have : g = pushout.inr (f ≫ g) f ≫ (asIso (pushout.inl (f ≫ g) f)).inv := by
      rw [asIso_inv, IsIso.eq_comp_inv, ← cancel_epi f, ← pushout.condition, assoc]
    rw [this, cancel_right_of_respectsIso (P := P)]
    exact P.pushout_inr _ _ hcomp

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