instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace

English

Criterion for equality of two injections into a colimit via opens.

Русский

Критерий равенства двух вложений в колимит через открытые множества.

LaTeX

$$$$ (colimit.ι F i).base \xi = (colimit.ι F j).base xj \iff \exists k fi fj, \exists x, (F.map fi).base x = \xi ∧ (F.map fj).base x = xj $$$$

Lean4

instance : PreservesColimit F Scheme.forgetToLocallyRingedSpace :=
  preservesColimit_of_preserves_colimit_cocone (isColimit F) (isColimitForgetToLocallyRingedSpace F)

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