instRespectsIsoScheme — Mathlib

English

If a morphism property P is HasAffineProperty with Q, then P respects isomorphisms of schemes; i.e., applying an isomorphism to the source and target preserves the property P.

Русский

Если свойство P объединено с Q через афинную локальность HasAffineProperty, то P сохраняется под изоморфизмами схем; т.е. применение изоморфизма к источнику и мишени сохраняет свойство P.

LaTeX

$$$[P, Q]\;\text{HasAffineProperty} \Rightarrow P\;\text{RespectsIso}$$$

Lean4

instance (priority := 900) : P.RespectsIso :=
  by
  letI := isLocal_affineProperty P
  rw [eq_targetAffineLocally P]
  infer_instance

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