affineAnd_respectsIso — Mathlib

English

The simplification lemma for affineAnd_apply states that the equivalence holds, i.e., affineAnd Q f iff IsAffine X ∧ Q (f.appTop).hom.

Русский

Лемма упрощения affineAnd_apply: affineAnd Q f эквивалентно IsAffine X ∧ Q (f.appTop).hom.

LaTeX

$$affineAnd_apply (Q) (f) : affineAnd Q f ↔ IsAffine X ∧ Q (f.appTop).hom$$

Lean4

/-- If `P` respects isos, also `affineAnd P` respects isomorphisms. -/
theorem affineAnd_respectsIso (hP : RingHom.RespectsIso Q) : (affineAnd Q).toProperty.RespectsIso :=
  by
  refine RespectsIso.mk _ ?_ ?_
  · intro X Y Z e f ⟨hZ, ⟨hY, hf⟩⟩
    simpa [hP.cancel_right_isIso, IsAffine.of_isIso e.hom]
  · intro X Y Z e f ⟨hZ, hf⟩
    simpa [AffineTargetMorphismProperty.toProperty, IsAffine.of_isIso e.inv, hP.cancel_left_isIso]

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