Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t

∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (i j : ι),
  (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).t i j = ⋯.symmetry ⋯

Defined in

Mathlib.AlgebraicGeometry.Sites.Representability

Cited by

0 results in Mathlib

Foundations

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