Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open

∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y)
  (U :
    TopologicalSpace.Opens
      ↑↑(CategoryTheory.Limits.coequalizer (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
              (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).toPresheafedSpace)
  (s :
    ↑((CategoryTheory.Limits.coequalizer (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
              (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).presheaf.obj
        (Opposite.op U))),
  IsOpen
    (⇑(CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.coequalizer.π (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
                (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).hom.base) ''
      (AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen f g U s).carrier)

Defined in

Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Cited by

0 results in Mathlib

Foundations

Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound