instRespectsIsoSchemeTargetAffineLocallyOfToProperty

English

Any property built from P via of P respects isomorphisms: the derived property preserves isomorphisms.

Русский

Любое свойство, полученное из P через конструкцию of, сохраняет изоморфизмы.

LaTeX

$$$\forall P [P.RespectsIso], (of P).toProperty.RespectsIso.$$$

Lean4

instance (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] : (targetAffineLocally P).RespectsIso :=
  by
  apply MorphismProperty.RespectsIso.mk
  · introv H U
    rw [morphismRestrict_comp, P.cancel_left_of_respectsIso]
    exact H U
  · introv H
    rintro ⟨U, hU : IsAffineOpen U⟩; dsimp
    haveI : IsAffine _ := hU.preimage_of_isIso e.hom
    rw [morphismRestrict_comp, P.cancel_right_of_respectsIso]
    exact H ⟨(Opens.map e.hom.base).obj U, hU.preimage_of_isIso e.hom⟩

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