mathlib3 documentation

category_theory.sites.grothendieck

Grothendieck topologies #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Definition and lemmas about Grothendieck topologies. A Grothendieck topology for a category C is a set of sieves on each object X satisfying certain closure conditions.

Alternate versions of the axioms (in arrow form) are also described. Two explicit examples of Grothendieck topologies are given:

A pretopology, or a basis for a topology is defined in pretopology.lean. The topology associated to a topological space is defined in spaces.lean.

Tags #

Grothendieck topology, coverage, pretopology, site

References #

Implementation notes #

We use the definition of [nlab] and [MM92][] (Chapter III, Section 2), where Grothendieck topologies are saturated collections of morphisms, rather than the notions of the Stacks project (00VG) and the Elephant, in which topologies are allowed to be unsaturated, and are then completed. TODO (BM): Add the definition from Stacks, as a pretopology, and complete to a topology.

This is so that we can produce a bijective correspondence between Grothendieck topologies on a small category and Lawvere-Tierney topologies on its presheaf topos, as well as the equivalence between Grothendieck topoi and left exact reflective subcategories of presheaf toposes.

source
structure category_theory.grothendieck_topology (C : Type u) [category_theory.category C] :
Type (max u v)

The definition of a Grothendieck topology: a set of sieves J X on each object X satisfying three axioms:

  1. For every object X, the maximal sieve is in J X.
  2. If S ∈ J X then its pullback along any h : Y ⟶ X is in J Y.
  3. If S ∈ J X and R is a sieve on X, then provided that the pullback of R along any arrow f : Y ⟶ X in S is in J Y, we have that R itself is in J X.

A sieve S on X is referred to as J-covering, (or just covering), if S ∈ J X.

See https://stacks.math.columbia.edu/tag/00Z4, or [nlab], or [MM92][] Chapter III, Section 2, Definition 1.

Instances for category_theory.grothendieck_topology
source
@[protected, instance]
def category_theory.grothendieck_topology.has_coe_to_fun (C : Type u) [category_theory.category C] :
has_coe_to_fun (category_theory.grothendieck_topology C) (λ (_x : category_theory.grothendieck_topology C), Π (X : C), set (category_theory.sieve X))
Equations
source
@[ext]
theorem category_theory.grothendieck_topology.ext {C : Type u} [category_theory.category C] {J₁ J₂ : category_theory.grothendieck_topology C} (h : ⇑J₁ = ⇑J₂) :
J₁ = J₂

An extensionality lemma in terms of the coercion to a pi-type. We prove this explicitly rather than deriving it so that it is in terms of the coercion rather than the projection .sieves.

source
@[simp]
theorem category_theory.grothendieck_topology.mem_sieves_iff_coe {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} (J : category_theory.grothendieck_topology C) :
S ∈ J.sieves X ↔ S ∈ ⇑J X
source
@[simp]
theorem category_theory.grothendieck_topology.top_mem {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (X : C) :
⊤ ∈ ⇑J X
source
@[simp]
theorem category_theory.grothendieck_topology.pullback_stable {C : Type u} [category_theory.category C] {X Y : C} {S : category_theory.sieve X} (J : category_theory.grothendieck_topology C) (f : Y ⟶ X) (hS : S ∈ ⇑J X) :
category_theory.sieve.pullback f S ∈ ⇑J Y
source
theorem category_theory.grothendieck_topology.transitive {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} (J : category_theory.grothendieck_topology C) (hS : S ∈ ⇑J X) (R : category_theory.sieve X) (h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⇑S f → category_theory.sieve.pullback f R ∈ ⇑J Y) :
R ∈ ⇑J X
source
theorem category_theory.grothendieck_topology.covering_of_eq_top {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} (J : category_theory.grothendieck_topology C) :
S = ⊤ → S ∈ ⇑J X
source
theorem category_theory.grothendieck_topology.superset_covering {C : Type u} [category_theory.category C] {X : C} {S R : category_theory.sieve X} (J : category_theory.grothendieck_topology C) (Hss : S ≤ R) (sjx : S ∈ ⇑J X) :
R ∈ ⇑J X

If S is a subset of R, and S is covering, then R is covering as well.

See https://stacks.math.columbia.edu/tag/00Z5 (2), or discussion after [MM92] Chapter III, Section 2, Definition 1.

source
theorem category_theory.grothendieck_topology.intersection_covering {C : Type u} [category_theory.category C] {X : C} {S R : category_theory.sieve X} (J : category_theory.grothendieck_topology C) (rj : R ∈ ⇑J X) (sj : S ∈ ⇑J X) :
R ⊓ S ∈ ⇑J X

The intersection of two covering sieves is covering.

See https://stacks.math.columbia.edu/tag/00Z5 (1), or [MM92] Chapter III, Section 2, Definition 1 (iv).

source
@[simp]
theorem category_theory.grothendieck_topology.intersection_covering_iff {C : Type u} [category_theory.category C] {X : C} {S R : category_theory.sieve X} (J : category_theory.grothendieck_topology C) :
R ⊓ S ∈ ⇑J X ↔ R ∈ ⇑J X ∧ S ∈ ⇑J X
source
theorem category_theory.grothendieck_topology.bind_covering {C : Type u} [category_theory.category C] {X : C} (J : category_theory.grothendieck_topology C) {S : category_theory.sieve X} {R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⇑S f → category_theory.sieve Y} (hS : S ∈ ⇑J X) (hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (H : ⇑S f), R H ∈ ⇑J Y) :
category_theory.sieve.bind ⇑S R ∈ ⇑J X
source
def category_theory.grothendieck_topology.covers {C : Type u} [category_theory.category C] {X Y : C} (J : category_theory.grothendieck_topology C) (S : category_theory.sieve X) (f : Y ⟶ X) :
Prop

The sieve S on X J-covers an arrow f to X if S.pullback f ∈ J Y. This definition is an alternate way of presenting a Grothendieck topology.

Equations
source
theorem category_theory.grothendieck_topology.covers_iff {C : Type u} [category_theory.category C] {X Y : C} (J : category_theory.grothendieck_topology C) (S : category_theory.sieve X) (f : Y ⟶ X) :
J.covers S f ↔ category_theory.sieve.pullback f S ∈ ⇑J Y
source
theorem category_theory.grothendieck_topology.covering_iff_covers_id {C : Type u} [category_theory.category C] {X : C} (J : category_theory.grothendieck_topology C) (S : category_theory.sieve X) :
S ∈ ⇑J X ↔ J.covers S (𝟙 X)
source
theorem category_theory.grothendieck_topology.arrow_max {C : Type u} [category_theory.category C] {X Y : C} (J : category_theory.grothendieck_topology C) (f : Y ⟶ X) (S : category_theory.sieve X) (hf : ⇑S f) :
J.covers S f

The maximality axiom in 'arrow' form: Any arrow f in S is covered by S.

source
theorem category_theory.grothendieck_topology.arrow_stable {C : Type u} [category_theory.category C] {X Y : C} (J : category_theory.grothendieck_topology C) (f : Y ⟶ X) (S : category_theory.sieve X) (h : J.covers S f) {Z : C} (g : Z ⟶ Y) :
J.covers S (g ≫ f)

The stability axiom in 'arrow' form: If S covers f then S covers g ≫ f for any g.

source
theorem category_theory.grothendieck_topology.arrow_trans {C : Type u} [category_theory.category C] {X Y : C} (J : category_theory.grothendieck_topology C) (f : Y ⟶ X) (S R : category_theory.sieve X) (h : J.covers S f) :
(∀ {Z : C} (g : Z ⟶ X), ⇑S g → J.covers R g) → J.covers R f

The transitivity axiom in 'arrow' form: If S covers f and every arrow in S is covered by R, then R covers f.

source
theorem category_theory.grothendieck_topology.arrow_intersect {C : Type u} [category_theory.category C] {X Y : C} (J : category_theory.grothendieck_topology C) (f : Y ⟶ X) (S R : category_theory.sieve X) (hS : J.covers S f) (hR : J.covers R f) :
J.covers (S ⊓ R) f
source
def category_theory.grothendieck_topology.trivial (C : Type u) [category_theory.category C] :
category_theory.grothendieck_topology C

The trivial Grothendieck topology, in which only the maximal sieve is covering. This topology is also known as the indiscrete, coarse, or chaotic topology.

See [MM92] Chapter III, Section 2, example (a), or https://en.wikipedia.org/wiki/Grothendieck_topology#The_discrete_and_indiscrete_topologies

Equations
source
def category_theory.grothendieck_topology.discrete (C : Type u) [category_theory.category C] :
category_theory.grothendieck_topology C

The discrete Grothendieck topology, in which every sieve is covering.

See https://en.wikipedia.org/wiki/Grothendieck_topology#The_discrete_and_indiscrete_topologies.

Equations
source
theorem category_theory.grothendieck_topology.trivial_covering {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} :
S ∈ ⇑(category_theory.grothendieck_topology.trivial C) X ↔ S = ⊤
source
@[protected, instance]
def category_theory.grothendieck_topology.has_le {C : Type u} [category_theory.category C] :
has_le (category_theory.grothendieck_topology C)

See https://stacks.math.columbia.edu/tag/00Z6

Equations
source
theorem category_theory.grothendieck_topology.le_def {C : Type u} [category_theory.category C] {J₁ J₂ : category_theory.grothendieck_topology C} :
J₁ ≤ J₂ ↔ ⇑J₁ ≤ ⇑J₂
source
@[protected, instance]
def category_theory.grothendieck_topology.partial_order {C : Type u} [category_theory.category C] :
partial_order (category_theory.grothendieck_topology C)

See https://stacks.math.columbia.edu/tag/00Z6

Equations
source
@[protected, instance]
def category_theory.grothendieck_topology.has_Inf {C : Type u} [category_theory.category C] :
has_Inf (category_theory.grothendieck_topology C)

See https://stacks.math.columbia.edu/tag/00Z7

Equations
source
theorem category_theory.grothendieck_topology.is_glb_Inf {C : Type u} [category_theory.category C] (s : set (category_theory.grothendieck_topology C)) :
is_glb s (has_Inf.Inf s)

See https://stacks.math.columbia.edu/tag/00Z7

source
@[protected, instance]
def category_theory.grothendieck_topology.complete_lattice {C : Type u} [category_theory.category C] :
complete_lattice (category_theory.grothendieck_topology C)

Construct a complete lattice from the Inf, but make the trivial and discrete topologies definitionally equal to the bottom and top respectively.

Equations
source
@[protected, instance]
def category_theory.grothendieck_topology.inhabited {C : Type u} [category_theory.category C] :
inhabited (category_theory.grothendieck_topology C)
Equations
source
@[simp]
theorem category_theory.grothendieck_topology.trivial_eq_bot {C : Type u} [category_theory.category C] :
category_theory.grothendieck_topology.trivial C = ⊥
source
@[simp]
theorem category_theory.grothendieck_topology.discrete_eq_top {C : Type u} [category_theory.category C] :
category_theory.grothendieck_topology.discrete C = ⊤
source
@[simp]
theorem category_theory.grothendieck_topology.bot_covering {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} :
S ∈ ⇑⊥ X ↔ S = ⊤
source
@[simp]
theorem category_theory.grothendieck_topology.top_covering {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} :
S ∈ ⇑⊤ X
source
theorem category_theory.grothendieck_topology.bot_covers {C : Type u} [category_theory.category C] {X Y : C} (S : category_theory.sieve X) (f : Y ⟶ X) :
⊥.covers S f ↔ ⇑S f
source
@[simp]
theorem category_theory.grothendieck_topology.top_covers {C : Type u} [category_theory.category C] {X Y : C} (S : category_theory.sieve X) (f : Y ⟶ X) :
⊤.covers S f
source
def category_theory.grothendieck_topology.dense {C : Type u} [category_theory.category C] :
category_theory.grothendieck_topology C

The dense Grothendieck topology.

See https://ncatlab.org/nlab/show/dense+topology, or [MM92] Chapter III, Section 2, example (e).

Equations
source
theorem category_theory.grothendieck_topology.dense_covering {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} :
S ∈ ⇑category_theory.grothendieck_topology.dense X ↔ ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), ⇑S (g ≫ f)
source
def category_theory.grothendieck_topology.right_ore_condition (C : Type u) [category_theory.category C] :
Prop

A category satisfies the right Ore condition if any span can be completed to a commutative square. NB. Any category with pullbacks obviously satisfies the right Ore condition, see right_ore_of_pullbacks.

Equations
source
theorem category_theory.grothendieck_topology.right_ore_of_pullbacks {C : Type u} [category_theory.category C] [category_theory.limits.has_pullbacks C] :
category_theory.grothendieck_topology.right_ore_condition C
source
def category_theory.grothendieck_topology.atomic {C : Type u} [category_theory.category C] (hro : category_theory.grothendieck_topology.right_ore_condition C) :
category_theory.grothendieck_topology C

The atomic Grothendieck topology: a sieve is covering iff it is nonempty. For the pullback stability condition, we need the right Ore condition to hold.

See https://ncatlab.org/nlab/show/atomic+site, or [MM92] Chapter III, Section 2, example (f).

Equations
source
@[protected, instance]
def category_theory.grothendieck_topology.cover.preorder {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (X : C) :
preorder (J.cover X)
source
def category_theory.grothendieck_topology.cover {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (X : C) :
Type (max u v)

J.cover X denotes the poset of covers of X with respect to the Grothendieck topology J.

Equations
Instances for category_theory.grothendieck_topology.cover
source
@[protected, instance]
def category_theory.grothendieck_topology.cover.category_theory.sieve.has_coe {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} :
has_coe (J.cover X) (category_theory.sieve X)
Equations
source
@[protected, instance]
def category_theory.grothendieck_topology.cover.has_coe_to_fun {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} :
has_coe_to_fun (J.cover X) (λ (S : J.cover X), Π ⦃Y : C⦄, (Y ⟶ X) → Prop)
Equations
source
@[simp]
theorem category_theory.grothendieck_topology.cover.coe_fun_coe {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} (S : J.cover X) (f : Y ⟶ X) :
⇑↑S f = ⇑S f
source
theorem category_theory.grothendieck_topology.cover.condition {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} (S : J.cover X) :
↑S ∈ ⇑J X
source
@[ext]
theorem category_theory.grothendieck_topology.cover.ext {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} (S T : J.cover X) (h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), ⇑S f ↔ ⇑T f) :
S = T
source
@[protected, instance]
def category_theory.grothendieck_topology.cover.order_top {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} :
order_top (J.cover X)
Equations
source
@[protected, instance]
def category_theory.grothendieck_topology.cover.semilattice_inf {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} :
semilattice_inf (J.cover X)
Equations
source
@[protected, instance]
def category_theory.grothendieck_topology.cover.inhabited {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} :
inhabited (J.cover X)
Equations
source
theorem category_theory.grothendieck_topology.cover.arrow.ext_iff {C : Type u} {_inst_1 : category_theory.category C} {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (x y : S.arrow) :
x = y ↔ x.Y = y.Y ∧ x.f == y.f
source
theorem category_theory.grothendieck_topology.cover.arrow.ext {C : Type u} {_inst_1 : category_theory.category C} {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (x y : S.arrow) (h : x.Y = y.Y) (h_1 : x.f == y.f) :
x = y
source
@[nolint, ext]
structure category_theory.grothendieck_topology.cover.arrow {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} (S : J.cover X) :
Type (max u v)
  • Y : C
  • f : self.Y ⟶ X
  • hf : ⇑S self.f

An auxiliary structure, used to define S.index in plus.lean.

Instances for category_theory.grothendieck_topology.cover.arrow
  • category_theory.grothendieck_topology.cover.arrow.has_sizeof_inst
source
theorem category_theory.grothendieck_topology.cover.relation.ext_iff {C : Type u} {_inst_1 : category_theory.category C} {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (x y : S.relation) :
x = y ↔ x.Y₁ = y.Y₁ ∧ x.Y₂ = y.Y₂ ∧ x.Z = y.Z ∧ x.g₁ == y.g₁ ∧ x.g₂ == y.g₂ ∧ x.f₁ == y.f₁ ∧ x.f₂ == y.f₂
source
@[nolint, ext]
structure category_theory.grothendieck_topology.cover.relation {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} (S : J.cover X) :
Type (max u v)

An auxiliary structure, used to define S.index in plus.lean.

Instances for category_theory.grothendieck_topology.cover.relation
  • category_theory.grothendieck_topology.cover.relation.has_sizeof_inst
source
theorem category_theory.grothendieck_topology.cover.relation.ext {C : Type u} {_inst_1 : category_theory.category C} {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (x y : S.relation) (h : x.Y₁ = y.Y₁) (h_1 : x.Y₂ = y.Y₂) (h_2 : x.Z = y.Z) (h_3 : x.g₁ == y.g₁) (h_4 : x.g₂ == y.g₂) (h_5 : x.f₁ == y.f₁) (h_6 : x.f₂ == y.f₂) :
x = y
source
@[simp]
theorem category_theory.grothendieck_topology.cover.arrow.map_f {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.arrow) (f : S ⟶ T) :
(I.map f).f = I.f
source
def category_theory.grothendieck_topology.cover.arrow.map {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.arrow) (f : S ⟶ T) :
T.arrow

Map a arrow along a refinement S ⟶ T.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.cover.arrow.map_Y {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.arrow) (f : S ⟶ T) :
(I.map f).Y = I.Y
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.map_Y₂ {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
(I.map f).Y₂ = I.Y₂
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.map_g₂ {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
(I.map f).g₂ = I.g₂
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.map_f₂ {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
(I.map f).f₂ = I.f₂
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.map_Y₁ {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
(I.map f).Y₁ = I.Y₁
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.map_g₁ {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
(I.map f).g₁ = I.g₁
source
def category_theory.grothendieck_topology.cover.relation.map {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
T.relation

Map a relation along a refinement S ⟶ T.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.map_Z {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
(I.map f).Z = I.Z
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.map_f₁ {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
(I.map f).f₁ = I.f₁
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.fst_f {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (I : S.relation) :
I.fst.f = I.f₁
source
def category_theory.grothendieck_topology.cover.relation.fst {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (I : S.relation) :
S.arrow

The first arrow associated to a relation. Used in defining index in plus.lean.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.fst_Y {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (I : S.relation) :
I.fst.Y = I.Y₁
source
def category_theory.grothendieck_topology.cover.relation.snd {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (I : S.relation) :
S.arrow

The second arrow associated to a relation. Used in defining index in plus.lean.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.snd_Y {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (I : S.relation) :
I.snd.Y = I.Y₂
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.snd_f {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S : J.cover X} (I : S.relation) :
I.snd.f = I.f₂
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.map_fst {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
I.fst.map f = (I.map f).fst
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.map_snd {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {S T : J.cover X} (I : S.relation) (f : S ⟶ T) :
I.snd.map f = (I.map f).snd
source
def category_theory.grothendieck_topology.cover.pullback {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} (S : J.cover X) (f : Y ⟶ X) :
J.cover Y

Pull back a cover along a morphism.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.cover.arrow.base_Y {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).arrow) :
I.base.Y = I.Y
source
@[simp]
theorem category_theory.grothendieck_topology.cover.arrow.base_f {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).arrow) :
I.base.f = I.f ≫ f
source
def category_theory.grothendieck_topology.cover.arrow.base {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).arrow) :
S.arrow

An arrow of S.pullback f gives rise to an arrow of S.

Equations
source
def category_theory.grothendieck_topology.cover.relation.base {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
S.relation

A relation of S.pullback f gives rise to a relation of S.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.base_Z {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
I.base.Z = I.Z
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.base_f₂ {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
I.base.f₂ = I.f₂ ≫ f
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.base_Y₁ {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
I.base.Y₁ = I.Y₁
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.base_g₁ {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
I.base.g₁ = I.g₁
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.base_g₂ {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
I.base.g₂ = I.g₂
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.base_f₁ {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
I.base.f₁ = I.f₁ ≫ f
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.base_Y₂ {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
I.base.Y₂ = I.Y₂
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.base_fst {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
I.fst.base = I.base.fst
source
@[simp]
theorem category_theory.grothendieck_topology.cover.relation.base_snd {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {f : Y ⟶ X} {S : J.cover X} (I : (S.pullback f).relation) :
I.snd.base = I.base.snd
source
@[simp]
theorem category_theory.grothendieck_topology.cover.coe_pullback {C : Type u} [category_theory.category C] {X Y : C} {J : category_theory.grothendieck_topology C} {Z : C} (f : Y ⟶ X) (g : Z ⟶ Y) (S : J.cover X) :
⇑(S.pullback f) g ↔ ⇑S (g ≫ f)
source
def category_theory.grothendieck_topology.cover.pullback_id {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} (S : J.cover X) :
S.pullback (𝟙 X) ≅ S

The isomorphism between S and the pullback of S w.r.t. the identity.

Equations
source
def category_theory.grothendieck_topology.cover.pullback_comp {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X Y Z : C} (S : J.cover X) (f : Z ⟶ Y) (g : Y ⟶ X) :
S.pullback (f ≫ g) ≅ (S.pullback g).pullback f

Pulling back with respect to a composition is the composition of the pullbacks.

Equations
source
def category_theory.grothendieck_topology.cover.bind {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} (S : J.cover X) (T : Π (I : S.arrow), J.cover I.Y) :
J.cover X

Combine a family of covers over a cover.

Equations
source
def category_theory.grothendieck_topology.cover.bind_to_base {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} (S : J.cover X) (T : Π (I : S.arrow), J.cover I.Y) :
S.bind T ⟶ S

The canonical moprhism from S.bind T to T.

Equations
source
noncomputable def category_theory.grothendieck_topology.cover.arrow.middle {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y} (I : (S.bind T).arrow) :
C

An arrow in bind has the form A ⟶ B ⟶ X where A ⟶ B is an arrow in T I for some I. and B ⟶ X is an arrow of S. This is the object B.

Equations
source
noncomputable def category_theory.grothendieck_topology.cover.arrow.to_middle_hom {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y} (I : (S.bind T).arrow) :
I.Y ⟶ I.middle

An arrow in bind has the form A ⟶ B ⟶ X where A ⟶ B is an arrow in T I for some I. and B ⟶ X is an arrow of S. This is the hom A ⟶ B.

Equations
source
noncomputable def category_theory.grothendieck_topology.cover.arrow.from_middle_hom {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y} (I : (S.bind T).arrow) :
I.middle ⟶ X

An arrow in bind has the form A ⟶ B ⟶ X where A ⟶ B is an arrow in T I for some I. and B ⟶ X is an arrow of S. This is the hom B ⟶ X.

Equations
source
theorem category_theory.grothendieck_topology.cover.arrow.from_middle_condition {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y} (I : (S.bind T).arrow) :
⇑S I.from_middle_hom
source
noncomputable def category_theory.grothendieck_topology.cover.arrow.from_middle {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y} (I : (S.bind T).arrow) :
S.arrow

An arrow in bind has the form A ⟶ B ⟶ X where A ⟶ B is an arrow in T I for some I. and B ⟶ X is an arrow of S. This is the hom B ⟶ X, as an arrow.

Equations
source
theorem category_theory.grothendieck_topology.cover.arrow.to_middle_condition {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y} (I : (S.bind T).arrow) :
⇑(T I.from_middle) I.to_middle_hom
source
noncomputable def category_theory.grothendieck_topology.cover.arrow.to_middle {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y} (I : (S.bind T).arrow) :
(T I.from_middle).arrow

An arrow in bind has the form A ⟶ B ⟶ X where A ⟶ B is an arrow in T I for some I. and B ⟶ X is an arrow of S. This is the hom A ⟶ B, as an arrow.

Equations
source
theorem category_theory.grothendieck_topology.cover.arrow.middle_spec {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y} (I : (S.bind T).arrow) :
I.to_middle_hom ≫ I.from_middle_hom = I.f
source
def category_theory.grothendieck_topology.cover.index {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] (S : J.cover X) (P : Cᵒᵖ ⥤ D) :
category_theory.limits.multicospan_index D

To every S : J.cover X and presheaf P, associate a multicospan_index.

Equations
source
@[reducible]
def category_theory.grothendieck_topology.cover.multifork {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] (S : J.cover X) (P : Cᵒᵖ ⥤ D) :
category_theory.limits.multifork (S.index P)

The natural multifork associated to S : J.cover X for a presheaf P. Saying that this multifork is a limit is essentially equivalent to the sheaf condition at the given object for the given covering sieve. See sheaf.lean for an equivalent sheaf condition using this.

source
@[reducible]
noncomputable def category_theory.grothendieck_topology.cover.to_multiequalizer {C : Type u} [category_theory.category C] {X : C} {J : category_theory.grothendieck_topology C} {D : Type w} [category_theory.category D] (S : J.cover X) (P : Cᵒᵖ ⥤ D) [category_theory.limits.has_multiequalizer (S.index P)] :
P.obj (opposite.op X) ⟶ category_theory.limits.multiequalizer (S.index P)

The canonical map from P.obj (op X) to the multiequalizer associated to a covering sieve, assuming such a multiequalizer exists. This will be used in sheaf.lean to provide an equivalent sheaf condition in terms of multiequalizers.

source
@[simp]
theorem category_theory.grothendieck_topology.pullback_obj {C : Type u} [category_theory.category C] {X Y : C} (J : category_theory.grothendieck_topology C) (f : Y ⟶ X) (S : J.cover X) :
(J.pullback f).obj S = S.pullback f
source
def category_theory.grothendieck_topology.pullback {C : Type u} [category_theory.category C] {X Y : C} (J : category_theory.grothendieck_topology C) (f : Y ⟶ X) :
J.cover X ⥤ J.cover Y

Pull back a cover along a morphism.

Equations
source
def category_theory.grothendieck_topology.pullback_id {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (X : C) :
J.pullback (𝟙 X) ≅ 𝟭 (J.cover X)

Pulling back along the identity is naturally isomorphic to the identity functor.

Equations
source
def category_theory.grothendieck_topology.pullback_comp {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
J.pullback (f ≫ g) ≅ J.pullback g ⋙ J.pullback f

Pulling back along a composition is naturally isomorphic to the composition of the pullbacks.

Equations