The category of points of a site

We define the category structure on the points of a site (C, J): a morphism between Φ₁ ⟶ Φ₂ between two points consists of a morphism Φ₂.fiber ⟶ Φ₁.fiber (SGA 4 IV 3.2).

References

• Alexander Grothendieck and Jean-Louis Verdier, Exposé IV : Topos, SGA 4 IV 3.2

structure CategoryTheory.GrothendieckTopology.Point.Hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ₁ Φ₂ : J.Point) : Type (max u w)

A morphism between points of a site consists of a morphism between the functors Point.fiber, in the opposite direction.

• hom : Φ₂.fiber ⟶ Φ₁.fiber

  a natural transformation, in the opposite direction

theorem CategoryTheory.GrothendieckTopology.Point.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {J : GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} {x y : Φ₁.Hom Φ₂} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.GrothendieckTopology.Point.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {J : GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} {x y : Φ₁.Hom Φ₂} (hom : x.hom = y.hom) : x = y

instance CategoryTheory.GrothendieckTopology.Point.instCategory {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} : Category.{max u w, max (max (w + 1) u) v} J.Point

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.GrothendieckTopology.Point.hom_ext {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} {f g : Φ₁ ⟶ Φ₂} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.GrothendieckTopology.Point.hom_ext_iff {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {Φ₁ Φ₂ : J.Point} {f g : Φ₁ ⟶ Φ₂} : f = g ↔ f.hom = g.hom

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.id_hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) : (CategoryStruct.id Φ).hom = CategoryStruct.id Φ.fiber

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.comp_hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) : (CategoryStruct.comp f g).hom = CategoryStruct.comp g.hom f.hom

theorem CategoryTheory.GrothendieckTopology.Point.comp_hom_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) {Z : Functor C (Type w)} (h : Φ₁.fiber ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).hom h = CategoryStruct.comp g.hom (CategoryStruct.comp f.hom h)

noncomputable def CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ : J.Point} (f : Φ₁ ⟶ Φ₂) : Φ₂.presheafFiber ⟶ Φ₁.presheafFiber

The natural transformation on fibers of presheaves that is induced by a morphism of points of a site.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_app {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ : J.Point} (f : Φ₁ ⟶ Φ₂) (P : Functor Cᵒᵖ A) : (presheafFiber f).app P = Φ₂.presheafFiberDesc (fun (X : C) (x : Φ₂.fiber.obj X) => Φ₁.toPresheafFiber X (f.hom.app X x) P) ⋯

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_id {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (Φ : J.Point) : presheafFiber (CategoryStruct.id Φ) = CategoryStruct.id Φ.presheafFiber

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_comp {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) : presheafFiber (CategoryStruct.comp f g) = CategoryStruct.comp (presheafFiber g) (presheafFiber f)

theorem CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_comp_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) {Z : Functor (Functor Cᵒᵖ A) A} (h : Φ₁.presheafFiber ⟶ Z) : CategoryStruct.comp (presheafFiber (CategoryStruct.comp f g)) h = CategoryStruct.comp (presheafFiber g) (CategoryStruct.comp (presheafFiber f) h)

@[reducible, inline]

noncomputable abbrev CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ : J.Point} (f : Φ₁ ⟶ Φ₂) : Φ₂.sheafFiber ⟶ Φ₁.sheafFiber

The natural transformation on fibers of sheaves that is induced by a morphism of points of a site.

Equations

• CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber f = (CategoryTheory.sheafToPresheaf J A).whiskerLeft (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber f)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_id {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (Φ : J.Point) : sheafFiber (CategoryStruct.id Φ) = CategoryStruct.id Φ.sheafFiber

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_comp {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) : sheafFiber (CategoryStruct.comp f g) = CategoryStruct.comp (sheafFiber g) (sheafFiber f)

theorem CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_comp_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) {Z : Functor (Sheaf J A) A} (h : Φ₁.sheafFiber ⟶ Z) : CategoryStruct.comp (sheafFiber (CategoryStruct.comp f g)) h = CategoryStruct.comp (sheafFiber g) (CategoryStruct.comp (sheafFiber f) h)