coproductCofan — Mathlib

English

Defines the basic open of the image of a section s under the coequalizer projection, i.e. the basic open in the target Y of the section π⋅s.

Русский

Определяет базовую открытую для образа секции s под проекции коэквализатора, т.е. базовую открытую в целевой пространстве Y для секции π⋅s.

LaTeX

$$imageBasicOpen : Opens Y := Y.toRingedSpace.basicOpen ( (coequalizer.π f.toShHom g.toShHom).c.app (op U) s )$$

Lean4

/-- The explicit coproduct cofan for `F : discrete ι ⥤ LocallyRingedSpace`. -/
noncomputable def coproductCofan : Cocone F where
  pt := coproduct F
  ι :=
    { app := fun j =>
        ⟨colimit.ι (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u}) (F ⋙ forgetToSheafedSpace) j, inferInstance⟩
      naturality := fun ⟨j⟩ ⟨j'⟩ ⟨⟨(f : j = j')⟩⟩ => by subst f; simp }

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