cancel_right_isIso — Mathlib

English

If a property P respects isomorphisms, then right-canceling by an isomorphism g does not affect P: P(g ∘ f) ⇔ P(f).

Русский

Если свойство P сохраняет изоморфизмы, то правый множитель-изоморфизм g не влияет на P: P(g ∘ f) ⇔ P(f).

LaTeX

$$$\forall f,g\,(\text{IsIso}(g)\Rightarrow P(g\circ f) \Leftrightarrow P(f)).$$$

Lean4

theorem cancel_right_isIso (hP : RespectsIso @P) {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsIso g] :
    P (g.hom.comp f.hom) ↔ P f.hom :=
  ⟨fun H => by
    convert hP.1 (f ≫ g).hom (asIso g).symm.commRingCatIsoToRingEquiv H
    simp [← CommRingCat.hom_comp], hP.1 f.hom (asIso g).commRingCatIsoToRingEquiv⟩

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