Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp

∀ {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)) {V U : AlgebraicGeometry.Scheme} (γ : V ⟶ U)
  (α : U ⟶ (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).glued),
  (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf).hom.app (Opposite.op V)))
      (CategoryTheory.CategoryStruct.comp γ α) =
    (CategoryTheory.ConcreteCategory.hom (F.obj.map γ.op))
      ((CategoryTheory.ConcreteCategory.hom
          ((AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf hf).hom.app (Opposite.op U)))
        α)

Defined in

Mathlib.AlgebraicGeometry.Sites.Representability

Cited by

0 results in Mathlib

Foundations

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