Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected.congr_simp

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

Defined in

Mathlib.AlgebraicGeometry.Cover.Directed

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAlgebraicGeometry.Scheme.Cover.LocallyDirected