cancel_right_of_respectsIso — Mathlib

English

If P respects isomorphisms, then P(f ≫ g) is equivalent to P(f) when g is an isomorphism and both target and source are affine as required by the context.

Русский

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

LaTeX

$$$P(f \gg g) \iff P(f) \text{ when } g \text{ is iso and } Z \text{ affine }$$$

Lean4

theorem cancel_right_of_respectsIso (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] {X Y Z : Scheme}
    (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] [IsAffine Z] [IsAffine Y] : P (f ≫ g) ↔ P f := by
  rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.cancel_right_of_respectsIso]

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