imageBasicOpen_image_preimage — Mathlib

English

There is a canonical HasCoequalizers structure in LocallyRingedSpace for all arrows, derived from the parallel pair construction.

Русский

Для LocallyRingedSpace существует структура HasCoequalizers для всех пар параллельных стрелок, получаемая из параллельной пары.

LaTeX

$$HasCoequalizers f g$$

Lean4

theorem imageBasicOpen_image_preimage :
    (coequalizer.π f.toShHom g.toShHom).base ⁻¹'
        ((coequalizer.π f.toShHom g.toShHom).base '' (imageBasicOpen f g U s).1) =
      (imageBasicOpen f g U s).1 :=
  by
  fapply Types.coequalizer_preimage_image_eq_of_preimage_eq f.base (g.base : X.carrier.1 ⟶ Y.carrier.1)
  · ext
    simp_rw [types_comp_apply, ← TopCat.comp_app, ← PresheafedSpace.comp_base]
    congr 3
    exact coequalizer.condition f.toShHom g.toShHom
  · apply isColimitCoforkMapOfIsColimit (forget TopCat)
    apply isColimitCoforkMapOfIsColimit (SheafedSpace.forget _)
    exact coequalizerIsCoequalizer f.toShHom g.toShHom
  · suffices
      (TopologicalSpace.Opens.map f.base).obj (imageBasicOpen f g U s) =
        (TopologicalSpace.Opens.map g.base).obj (imageBasicOpen f g U s)
      by injection this
    delta imageBasicOpen
    rw [preimage_basicOpen f, preimage_basicOpen g]
    dsimp only [Functor.op, unop_op]
      -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): change `rw` to `erw`

    erw [← CommRingCat.comp_apply, ← SheafedSpace.comp_c_app', ← CommRingCat.comp_apply, ← SheafedSpace.comp_c_app',
      SheafedSpace.congr_app (coequalizer.condition f.toShHom g.toShHom), CommRingCat.comp_apply,
      X.toRingedSpace.basicOpen_res]
    apply inf_eq_right.mpr
    refine (RingedSpace.basicOpen_le _ _).trans ?_
    rw [coequalizer.condition f.toShHom g.toShHom]

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