cancel_left_isIso — Mathlib

English

If a property P respects isomorphisms, then composing on the left with an isomorphism does not change whether P holds; i.e., P(g∘f) is equivalent to P(g) when f is an isomorphism.

Русский

Если свойство P сохраняет изоморфизмы, композиция слева с изоморфизмом не меняет истинность P; P(g∘f) эквивалентно P(g) когда f — изоморфизм.

LaTeX

$$$P(g\\circ f) \\iff P(g)$ при $f$ изоморфизм.$$

Lean4

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

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