Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf

∀ {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 : ι),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.yoneda.map (AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf i))
      (AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf).hom =
    f i

Defined in

Mathlib.AlgebraicGeometry.Sites.Representability

Cited by

2 results in Mathlib

Foundations

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