imageBasicOpen_image_open — Mathlib

English

There is a HasColimits instance for LocallyRingedSpace with shape given by discrete categories, ensuring existence of coproducts and coequalizers in that setting.

Русский

Существует инстанс HasColimits для LocallyRingedSpace с формой дискретной категории, обеспечивающий существование копроизведений и коэквализаторов в этом окружении.

LaTeX

$$HasColimitsOfShape (Discrete ι) LocallyRingedSpace$$

Lean4

theorem imageBasicOpen_image_open : IsOpen ((coequalizer.π f.toShHom g.toShHom).base '' (imageBasicOpen f g U s).1) :=
  by
  rw [← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.toShHom g.toShHom)).isOpen_preimage,
    TopCat.coequalizer_isOpen_iff, ← Set.preimage_comp]
  erw [← TopCat.coe_comp]
  rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]
  dsimp only [SheafedSpace.forget]
  rw [imageBasicOpen_image_preimage]
  exact (imageBasicOpen f g U s).2

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