Theorems · Definition · algebraic geometry

AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.PresheafedSpace.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasLimits C] →
        (i j : D.J) →
          (U : TopologicalSpace.Opens ↑↑(D.U i)) →
            (D.U i).presheaf.obj (Opposite.op U) ⟶
              (D.U j).presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))

(Implementation). The map Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{U_j}, 𝖣.ι j ⁻¹' 𝖣.ι i '' U)

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasLimits