Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage

∀ {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))),
  ⇑(CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.coequalizer.π (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
                (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).hom.base) ⁻¹'
      ⇑(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 =
    (AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen f g U s).carrier

Defined in

Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Cited by

1 results in Mathlib

Foundations

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