Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected.congr_simp

∀ {S : AlgebraicGeometry.Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover)
  [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  {Y : CategoryTheory.Over S} (g g_1 : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left) (e_g : g = g_1)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i)
  (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom),
  𝒰.glueMorphismsOverOfLocallyDirected g h w = 𝒰.glueMorphismsOverOfLocallyDirected g_1 ⋯ ⋯

Defined in

Mathlib.AlgebraicGeometry.Cover.Directed

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.Scheme.Cover.LocallyDirected