instHasAffinePropertyDiagonalSchemeDiagonal

English

If HasAffineProperty holds for P and Q, then HasAffineProperty P.diagonal Q.diagonal.

Русский

Если HasAffineProperty держится для P и Q, то HasAffineProperty P.diagonal Q.diagonal.

LaTeX

$$HasAffineProperty P.diagonal Q.diagonal$$

Lean4

instance (P) {Q} [HasAffineProperty P Q] : HasAffineProperty P.diagonal Q.diagonal
    where
  isLocal_affineProperty :=
    letI := HasAffineProperty.isLocal_affineProperty P;
    inferInstance
  eq_targetAffineLocally' := by
    ext X Y f
    letI := HasAffineProperty.isLocal_affineProperty P
    constructor
    · exact fun H U ↦ HasAffineProperty.diagonal_of_diagonal_of_isPullback P (isPullback_morphismRestrict f U).flip H
    ·
      exact fun H ↦
        HasAffineProperty.diagonal_of_openCover_diagonal P f Y.affineCover
          (fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) H)

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