Theorems · Theorem · algebraic geometry

AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  (i j k : D.J) (S : Set ↑↑(D.V (i, j))),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k)).base) ''
      ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).base) ⁻¹' S =
    ⇑(CategoryTheory.ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(CategoryTheory.ConcreteCategory.hom (D.f i j).base) '' S

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category