Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected

∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] {Y : AlgebraicGeometry.Scheme}
  (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i)
  (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f i) (𝒰.glueMorphismsOfLocallyDirected g ⋯) = g i

Defined in

Mathlib.AlgebraicGeometry.Cover.Directed

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.Scheme.Cover.LocallyDirected