Theorems · Definition · algebraic geometry

TopCat.Sheaf.objSupIsoProdEqLocus

{X : TopCat} →
  (F : TopCat.Sheaf CommRingCat X) →
    (U V : TopologicalSpace.Opens ↑X) →
      F.obj.obj (Opposite.op (U ⊔ V)) ≅
        CommRingCat.of
          ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
                  (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus
              ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
                (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))))

F(U ⊔ V) is isomorphic to the eq_locus of the two maps F(U) × F(V) ⟶ F(U ⊓ V).

Defined in

Mathlib.Topology.Sheaves.CommRingCat

Cited by

6 results in Mathlib

Foundations

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