Grothendieck topologies

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:

• The dense topology
• The atomic topology as well as the complete lattice structure on Grothendieck topologies (which gives two additional explicit topologies: the discrete and trivial topologies.)

A pretopology, or a basis for a topology is defined in Mathlib/CategoryTheory/Sites/Pretopology.lean. The topology associated to a topological space is defined in Mathlib/CategoryTheory/Sites/Spaces.lean.

Tags

Grothendieck topology, coverage, pretopology, site

References

• nLab, Grothendieck topology
• [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]

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.

structure CategoryTheory.GrothendieckTopology (C : Type u) [CategoryTheory.Category.{v, u} 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 , or [nlab], or [MM92][] Chapter III, Section 2, Definition 1.

• sieves : (X : C) → Set (CategoryTheory.Sieve X)

  A Grothendieck topology on C consists of a set of sieves for each object X, which satisfy some axioms.

• top_mem' : ∀ (X : C), ⊤ ∈ self.sieves X

  The sieves associated to each object must contain the top sieve. Use GrothendieckTopology.top_mem.

• pullback_stable' : ∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X), S ∈ self.sieves X → CategoryTheory.Sieve.pullback f S ∈ self.sieves Y

  Stability under pullback. Use GrothendieckTopology.pullback_stable.

• transitive' : ∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄, S ∈ self.sieves X → ∀ (R : CategoryTheory.Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ self.sieves Y) → R ∈ self.sieves X

  Transitivity of sieves in a Grothendieck topology. Use GrothendieckTopology.transitive.

instance CategoryTheory.GrothendieckTopology.instCoeFunGrothendieckTopologyForAllSetSieve (C : Type u) [CategoryTheory.Category.{v, u} C] : CoeFun (CategoryTheory.GrothendieckTopology C) fun (x : CategoryTheory.GrothendieckTopology C) => (X : C) → Set (CategoryTheory.Sieve X)

Equations

• CategoryTheory.GrothendieckTopology.instCoeFunGrothendieckTopologyForAllSetSieve C = { coe := CategoryTheory.GrothendieckTopology.sieves }

theorem CategoryTheory.GrothendieckTopology.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {J₁ : CategoryTheory.GrothendieckTopology C} {J₂ : CategoryTheory.GrothendieckTopology C} (h : J₁.sieves = J₂.sieves) : 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.

@[simp]

theorem CategoryTheory.GrothendieckTopology.top_mem {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : ⊤ ∈ J.sieves X

Also known as the maximality axiom.

@[simp]

theorem CategoryTheory.GrothendieckTopology.pullback_stable {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {S : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (hS : S ∈ J.sieves X) : CategoryTheory.Sieve.pullback f S ∈ J.sieves Y

Also known as the stability axiom.

theorem CategoryTheory.GrothendieckTopology.transitive {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) (hS : S ∈ J.sieves X) (R : CategoryTheory.Sieve X) (h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ J.sieves Y) : R ∈ J.sieves X

theorem CategoryTheory.GrothendieckTopology.covering_of_eq_top {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) : S = ⊤ → S ∈ J.sieves X

theorem CategoryTheory.GrothendieckTopology.superset_covering {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} {R : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) (Hss : S ≤ R) (sjx : S ∈ J.sieves X) : R ∈ J.sieves X

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

See (2), or discussion after [MM92] Chapter III, Section 2, Definition 1.

theorem CategoryTheory.GrothendieckTopology.intersection_covering {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} {R : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) (rj : R ∈ J.sieves X) (sj : S ∈ J.sieves X) : R ⊓ S ∈ J.sieves X

The intersection of two covering sieves is covering.

See (1), or [MM92] Chapter III, Section 2, Definition 1 (iv).

@[simp]

theorem CategoryTheory.GrothendieckTopology.intersection_covering_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} {R : CategoryTheory.Sieve X} (J : CategoryTheory.GrothendieckTopology C) : R ⊓ S ∈ J.sieves X ↔ R ∈ J.sieves X ∧ S ∈ J.sieves X

theorem CategoryTheory.GrothendieckTopology.bind_covering {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (J : CategoryTheory.GrothendieckTopology C) {S : CategoryTheory.Sieve X} {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → CategoryTheory.Sieve Y} (hS : S ∈ J.sieves X) (hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (H : S.arrows f), R H ∈ J.sieves Y) : CategoryTheory.Sieve.bind S.arrows R ∈ J.sieves X

def CategoryTheory.GrothendieckTopology.Covers {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.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

• CategoryTheory.GrothendieckTopology.Covers J S f = (CategoryTheory.Sieve.pullback f S ∈ J.sieves Y)

theorem CategoryTheory.GrothendieckTopology.covers_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) (f : Y ⟶ X) : CategoryTheory.GrothendieckTopology.Covers J S f ↔ CategoryTheory.Sieve.pullback f S ∈ J.sieves Y

theorem CategoryTheory.GrothendieckTopology.covering_iff_covers_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (J : CategoryTheory.GrothendieckTopology C) (S : CategoryTheory.Sieve X) : S ∈ J.sieves X ↔ CategoryTheory.GrothendieckTopology.Covers J S (CategoryTheory.CategoryStruct.id X)

theorem CategoryTheory.GrothendieckTopology.arrow_max {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (S : CategoryTheory.Sieve X) (hf : S.arrows f) : CategoryTheory.GrothendieckTopology.Covers J S f

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

theorem CategoryTheory.GrothendieckTopology.arrow_stable {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (S : CategoryTheory.Sieve X) (h : CategoryTheory.GrothendieckTopology.Covers J S f) {Z : C} (g : Z ⟶ Y) : CategoryTheory.GrothendieckTopology.Covers J S (CategoryTheory.CategoryStruct.comp g f)

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

theorem CategoryTheory.GrothendieckTopology.arrow_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (S : CategoryTheory.Sieve X) (R : CategoryTheory.Sieve X) (h : CategoryTheory.GrothendieckTopology.Covers J S f) : (∀ {Z : C} (g : Z ⟶ X), S.arrows g → CategoryTheory.GrothendieckTopology.Covers J R g) → CategoryTheory.GrothendieckTopology.Covers J 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.

theorem CategoryTheory.GrothendieckTopology.arrow_intersect {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (S : CategoryTheory.Sieve X) (R : CategoryTheory.Sieve X) (hS : CategoryTheory.GrothendieckTopology.Covers J S f) (hR : CategoryTheory.GrothendieckTopology.Covers J R f) : CategoryTheory.GrothendieckTopology.Covers J (S ⊓ R) f

def CategoryTheory.GrothendieckTopology.trivial (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.GrothendieckTopology 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

• CategoryTheory.GrothendieckTopology.trivial C = { sieves := fun (X : C) => {⊤}, top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }

def CategoryTheory.GrothendieckTopology.discrete (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.GrothendieckTopology 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

• CategoryTheory.GrothendieckTopology.discrete C = { sieves := fun (X : C) => Set.univ, top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }

theorem CategoryTheory.GrothendieckTopology.trivial_covering {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} : S ∈ (CategoryTheory.GrothendieckTopology.trivial C).sieves X ↔ S = ⊤

instance CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology {C : Type u} [CategoryTheory.Category.{v, u} C] : LE (CategoryTheory.GrothendieckTopology C)

See

Equations

• CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology = { le := fun (J₁ J₂ : CategoryTheory.GrothendieckTopology C) => J₁.sieves ≤ J₂.sieves }

theorem CategoryTheory.GrothendieckTopology.le_def {C : Type u} [CategoryTheory.Category.{v, u} C] {J₁ : CategoryTheory.GrothendieckTopology C} {J₂ : CategoryTheory.GrothendieckTopology C} : J₁ ≤ J₂ ↔ J₁.sieves ≤ J₂.sieves

instance CategoryTheory.GrothendieckTopology.instPartialOrderGrothendieckTopology {C : Type u} [CategoryTheory.Category.{v, u} C] : PartialOrder (CategoryTheory.GrothendieckTopology C)

See

Equations

• CategoryTheory.GrothendieckTopology.instPartialOrderGrothendieckTopology = let __src := CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology; PartialOrder.mk ⋯

instance CategoryTheory.GrothendieckTopology.instInfSetGrothendieckTopology {C : Type u} [CategoryTheory.Category.{v, u} C] : InfSet (CategoryTheory.GrothendieckTopology C)

See

Equations

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

theorem CategoryTheory.GrothendieckTopology.isGLB_sInf {C : Type u} [CategoryTheory.Category.{v, u} C] (s : Set (CategoryTheory.GrothendieckTopology C)) : IsGLB s (sInf s)

See

instance CategoryTheory.GrothendieckTopology.instCompleteLatticeGrothendieckTopology {C : Type u} [CategoryTheory.Category.{v, u} C] : CompleteLattice (CategoryTheory.GrothendieckTopology C)

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

Equations

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

instance CategoryTheory.GrothendieckTopology.instInhabitedGrothendieckTopology {C : Type u} [CategoryTheory.Category.{v, u} C] : Inhabited (CategoryTheory.GrothendieckTopology C)

Equations

• CategoryTheory.GrothendieckTopology.instInhabitedGrothendieckTopology = { default := ⊤ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.trivial_eq_bot {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.GrothendieckTopology.trivial C = ⊥

@[simp]

theorem CategoryTheory.GrothendieckTopology.discrete_eq_top {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.GrothendieckTopology.discrete C = ⊤

@[simp]

theorem CategoryTheory.GrothendieckTopology.bot_covering {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} : S ∈ ⊥.sieves X ↔ S = ⊤

@[simp]

theorem CategoryTheory.GrothendieckTopology.top_covering {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} : S ∈ ⊤.sieves X

theorem CategoryTheory.GrothendieckTopology.bot_covers {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) : CategoryTheory.GrothendieckTopology.Covers ⊥ S f ↔ S.arrows f

@[simp]

theorem CategoryTheory.GrothendieckTopology.top_covers {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X) : CategoryTheory.GrothendieckTopology.Covers ⊤ S f

def CategoryTheory.GrothendieckTopology.dense {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.GrothendieckTopology C

The dense Grothendieck topology.

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

Equations

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

theorem CategoryTheory.GrothendieckTopology.dense_covering {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X} : S ∈ CategoryTheory.GrothendieckTopology.dense.sieves X ↔ ∀ {Y : C} (f : Y ⟶ X), ∃ (Z : C) (g : Z ⟶ Y), S.arrows (CategoryTheory.CategoryStruct.comp g f)

def CategoryTheory.GrothendieckTopology.RightOreCondition (C : Type u) [CategoryTheory.Category.{v, u} 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

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

theorem CategoryTheory.GrothendieckTopology.right_ore_of_pullbacks {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.GrothendieckTopology.RightOreCondition C

def CategoryTheory.GrothendieckTopology.atomic {C : Type u} [CategoryTheory.Category.{v, u} C] (hro : CategoryTheory.GrothendieckTopology.RightOreCondition C) : CategoryTheory.GrothendieckTopology 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

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

def CategoryTheory.GrothendieckTopology.Cover {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology 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

• CategoryTheory.GrothendieckTopology.Cover J X = { S : CategoryTheory.Sieve X // S ∈ J.sieves X }

instance CategoryTheory.GrothendieckTopology.instPreorderCover {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : Preorder (CategoryTheory.GrothendieckTopology.Cover J X)

Equations

• CategoryTheory.GrothendieckTopology.instPreorderCover J X = let_fun this := inferInstance; this

def CategoryTheory.GrothendieckTopology.Cover.sieve {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.GrothendieckTopology.Cover J X) : CategoryTheory.Sieve X

The sieve associated to a term of J.Cover X.

Equations

• CategoryTheory.GrothendieckTopology.Cover.sieve S = ↑S

instance CategoryTheory.GrothendieckTopology.Cover.instCoeFunCoverForAllHomToQuiverToCategoryStructProp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} : CoeFun (CategoryTheory.GrothendieckTopology.Cover J X) fun (x : CategoryTheory.GrothendieckTopology.Cover J X) => ⦃Y : C⦄ → (Y ⟶ X) → Prop

Equations

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

theorem CategoryTheory.GrothendieckTopology.Cover.condition {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.GrothendieckTopology.Cover J X) : CategoryTheory.GrothendieckTopology.Cover.sieve S ∈ J.sieves X

theorem CategoryTheory.GrothendieckTopology.Cover.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (T : CategoryTheory.GrothendieckTopology.Cover J X) (h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), (CategoryTheory.GrothendieckTopology.Cover.sieve S).arrows f ↔ (CategoryTheory.GrothendieckTopology.Cover.sieve T).arrows f) : S = T

instance CategoryTheory.GrothendieckTopology.Cover.instOrderTopCoverToLEInstPreorderCover {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} : OrderTop (CategoryTheory.GrothendieckTopology.Cover J X)

Equations

• CategoryTheory.GrothendieckTopology.Cover.instOrderTopCoverToLEInstPreorderCover = let __src := inferInstance; OrderTop.mk ⋯

instance CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInfCover {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} : SemilatticeInf (CategoryTheory.GrothendieckTopology.Cover J X)

Equations

• CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInfCover = let __src := inferInstance; SemilatticeInf.mk ⋯ ⋯ ⋯

instance CategoryTheory.GrothendieckTopology.Cover.instInhabitedCover {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} : Inhabited (CategoryTheory.GrothendieckTopology.Cover J X)

Equations

• CategoryTheory.GrothendieckTopology.Cover.instInhabitedCover = { default := ⊤ }

theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.ext_iff {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x y : CategoryTheory.GrothendieckTopology.Cover.Arrow S), x = y ↔ x.Y = y.Y ∧ HEq x.f y.f

theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.ext {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x y : CategoryTheory.GrothendieckTopology.Cover.Arrow S), x.Y = y.Y → HEq x.f y.f → x = y

structure CategoryTheory.GrothendieckTopology.Cover.Arrow {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.GrothendieckTopology.Cover J X) : Type (max u v)

An auxiliary structure, used to define S.index.

• Y : C

  The source of the arrow.

• f : self.Y ⟶ X

  The arrow itself.

• hf : (CategoryTheory.GrothendieckTopology.Cover.sieve S).arrows self.f

  The given arrow is contained in the given sieve.

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.ext_iff {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x y : CategoryTheory.GrothendieckTopology.Cover.Relation S), x = y ↔ x.Y₁ = y.Y₁ ∧ x.Y₂ = y.Y₂ ∧ x.Z = y.Z ∧ HEq x.g₁ y.g₁ ∧ HEq x.g₂ y.g₂ ∧ HEq x.f₁ y.f₁ ∧ HEq x.f₂ y.f₂

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.ext {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (x y : CategoryTheory.GrothendieckTopology.Cover.Relation S), x.Y₁ = y.Y₁ → x.Y₂ = y.Y₂ → x.Z = y.Z → HEq x.g₁ y.g₁ → HEq x.g₂ y.g₂ → HEq x.f₁ y.f₁ → HEq x.f₂ y.f₂ → x = y

structure CategoryTheory.GrothendieckTopology.Cover.Relation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.GrothendieckTopology.Cover J X) : Type (max u v)

An auxiliary structure, used to define S.index.

• Y₁ : C

  The source of the first arrow.

• Y₂ : C

  The source of the second arrow.

• Z : C

  The source of the arrows defining the relation.

• g₁ : self.Z ⟶ self.Y₁

  The first arrow defining the relation.

• g₂ : self.Z ⟶ self.Y₂

  The second arrow defining the relation.

• f₁ : self.Y₁ ⟶ X

  The first arrow which is part of the relation.

• f₂ : self.Y₂ ⟶ X

  The second arrow which is part of the relation.

• h₁ : (CategoryTheory.GrothendieckTopology.Cover.sieve S).arrows self.f₁

  The first arrow which is part of the relation is contained in the given sieve.

• h₂ : (CategoryTheory.GrothendieckTopology.Cover.sieve S).arrows self.f₂

  The second arrow which is part of the relation is contained in the given sieve.

• w : CategoryTheory.CategoryStruct.comp self.g₁ self.f₁ = CategoryTheory.CategoryStruct.comp self.g₂ self.f₂

  The relation itself.

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.w_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (self : CategoryTheory.GrothendieckTopology.Cover.Relation S) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp self.g₁ (CategoryTheory.CategoryStruct.comp self.f₁ h) = CategoryTheory.CategoryStruct.comp self.g₂ (CategoryTheory.CategoryStruct.comp self.f₂ h)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.map_f {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) (f : S ⟶ T) : (CategoryTheory.GrothendieckTopology.Cover.Arrow.map I f).f = I.f

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.map_Y {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) (f : S ⟶ T) : (CategoryTheory.GrothendieckTopology.Cover.Arrow.map I f).Y = I.Y

def CategoryTheory.GrothendieckTopology.Cover.Arrow.map {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) (f : S ⟶ T) : CategoryTheory.GrothendieckTopology.Cover.Arrow T

Map an Arrow along a refinement S ⟶ T.

Equations

• CategoryTheory.GrothendieckTopology.Cover.Arrow.map I f = { Y := I.Y, f := I.f, hf := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_Y₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f).Y₂ = I.Y₂

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f).f₁ = I.f₁

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_Y₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f).Y₁ = I.Y₁

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_g₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f).g₂ = I.g₂

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_Z {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f).Z = I.Z

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_g₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f).g₁ = I.g₁

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_f₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f).f₂ = I.f₂

def CategoryTheory.GrothendieckTopology.Cover.Relation.map {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : CategoryTheory.GrothendieckTopology.Cover.Relation T

Map a Relation along a refinement S ⟶ T.

Equations

• CategoryTheory.GrothendieckTopology.Cover.Relation.map I f = { Y₁ := I.Y₁, Y₂ := I.Y₂, Z := I.Z, g₁ := I.g₁, g₂ := I.g₂, f₁ := I.f₁, f₂ := I.f₂, h₁ := ⋯, h₂ := ⋯, w := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.fst_Y {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) : (CategoryTheory.GrothendieckTopology.Cover.Relation.fst I).Y = I.Y₁

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.fst_f {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) : (CategoryTheory.GrothendieckTopology.Cover.Relation.fst I).f = I.f₁

def CategoryTheory.GrothendieckTopology.Cover.Relation.fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) : CategoryTheory.GrothendieckTopology.Cover.Arrow S

The first Arrow associated to a Relation. Used in defining index.

Equations

• CategoryTheory.GrothendieckTopology.Cover.Relation.fst I = { Y := I.Y₁, f := I.f₁, hf := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.snd_Y {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) : (CategoryTheory.GrothendieckTopology.Cover.Relation.snd I).Y = I.Y₂

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.snd_f {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) : (CategoryTheory.GrothendieckTopology.Cover.Relation.snd I).f = I.f₂

def CategoryTheory.GrothendieckTopology.Cover.Relation.snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) : CategoryTheory.GrothendieckTopology.Cover.Arrow S

The second Arrow associated to a Relation. Used in defining index.

Equations

• CategoryTheory.GrothendieckTopology.Cover.Relation.snd I = { Y := I.Y₂, f := I.f₂, hf := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : CategoryTheory.GrothendieckTopology.Cover.Arrow.map (CategoryTheory.GrothendieckTopology.Cover.Relation.fst I) f = CategoryTheory.GrothendieckTopology.Cover.Relation.fst (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation S) (f : S ⟶ T) : CategoryTheory.GrothendieckTopology.Cover.Arrow.map (CategoryTheory.GrothendieckTopology.Cover.Relation.snd I) f = CategoryTheory.GrothendieckTopology.Cover.Relation.snd (CategoryTheory.GrothendieckTopology.Cover.Relation.map I f)

def CategoryTheory.GrothendieckTopology.Cover.pullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (f : Y ⟶ X) : CategoryTheory.GrothendieckTopology.Cover J Y

Pull back a cover along a morphism.

Equations

• CategoryTheory.GrothendieckTopology.Cover.pullback S f = { val := CategoryTheory.Sieve.pullback f (CategoryTheory.GrothendieckTopology.Cover.sieve S), property := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.base_f {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : (CategoryTheory.GrothendieckTopology.Cover.Arrow.base I).f = CategoryTheory.CategoryStruct.comp I.f f

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.base_Y {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : (CategoryTheory.GrothendieckTopology.Cover.Arrow.base I).Y = I.Y

def CategoryTheory.GrothendieckTopology.Cover.Arrow.base {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : CategoryTheory.GrothendieckTopology.Cover.Arrow S

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

Equations

• CategoryTheory.GrothendieckTopology.Cover.Arrow.base I = { Y := I.Y, f := CategoryTheory.CategoryStruct.comp I.f f, hf := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_Y₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : (CategoryTheory.GrothendieckTopology.Cover.Relation.base I).Y₁ = I.Y₁

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_g₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : (CategoryTheory.GrothendieckTopology.Cover.Relation.base I).g₂ = I.g₂

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_Z {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : (CategoryTheory.GrothendieckTopology.Cover.Relation.base I).Z = I.Z

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_f₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : (CategoryTheory.GrothendieckTopology.Cover.Relation.base I).f₁ = CategoryTheory.CategoryStruct.comp I.f₁ f

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_Y₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : (CategoryTheory.GrothendieckTopology.Cover.Relation.base I).Y₂ = I.Y₂

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_g₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : (CategoryTheory.GrothendieckTopology.Cover.Relation.base I).g₁ = I.g₁

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_f₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : (CategoryTheory.GrothendieckTopology.Cover.Relation.base I).f₂ = CategoryTheory.CategoryStruct.comp I.f₂ f

def CategoryTheory.GrothendieckTopology.Cover.Relation.base {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : CategoryTheory.GrothendieckTopology.Cover.Relation S

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

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : CategoryTheory.GrothendieckTopology.Cover.Arrow.base (CategoryTheory.GrothendieckTopology.Cover.Relation.fst I) = CategoryTheory.GrothendieckTopology.Cover.Relation.fst (CategoryTheory.GrothendieckTopology.Cover.Relation.base I)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {f : Y ⟶ X} {S : CategoryTheory.GrothendieckTopology.Cover J X} (I : CategoryTheory.GrothendieckTopology.Cover.Relation (CategoryTheory.GrothendieckTopology.Cover.pullback S f)) : CategoryTheory.GrothendieckTopology.Cover.Arrow.base (CategoryTheory.GrothendieckTopology.Cover.Relation.snd I) = CategoryTheory.GrothendieckTopology.Cover.Relation.snd (CategoryTheory.GrothendieckTopology.Cover.Relation.base I)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.coe_pullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {J : CategoryTheory.GrothendieckTopology C} {Z : C} (f : Y ⟶ X) (g : Z ⟶ Y) (S : CategoryTheory.GrothendieckTopology.Cover J X) : (CategoryTheory.GrothendieckTopology.Cover.sieve (CategoryTheory.GrothendieckTopology.Cover.pullback S f)).arrows g ↔ (CategoryTheory.GrothendieckTopology.Cover.sieve S).arrows (CategoryTheory.CategoryStruct.comp g f)

def CategoryTheory.GrothendieckTopology.Cover.pullbackId {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} (S : CategoryTheory.GrothendieckTopology.Cover J X) : CategoryTheory.GrothendieckTopology.Cover.pullback S (CategoryTheory.CategoryStruct.id X) ≅ S

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

Equations

• CategoryTheory.GrothendieckTopology.Cover.pullbackId S = CategoryTheory.eqToIso ⋯

def CategoryTheory.GrothendieckTopology.Cover.pullbackComp {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {Y : C} {Z : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (f : Z ⟶ Y) (g : Y ⟶ X) : CategoryTheory.GrothendieckTopology.Cover.pullback S (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.GrothendieckTopology.Cover.pullback (CategoryTheory.GrothendieckTopology.Cover.pullback S g) f

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

Equations

• CategoryTheory.GrothendieckTopology.Cover.pullbackComp S f g = CategoryTheory.eqToIso ⋯

def CategoryTheory.GrothendieckTopology.Cover.bind {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y) : CategoryTheory.GrothendieckTopology.Cover J X

Combine a family of covers over a cover.

Equations

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

def CategoryTheory.GrothendieckTopology.Cover.bindToBase {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y) : CategoryTheory.GrothendieckTopology.Cover.bind S T ⟶ S

The canonical morphism from S.bind T to T.

Equations

• CategoryTheory.GrothendieckTopology.Cover.bindToBase S T = CategoryTheory.homOfLE ⋯

noncomputable def CategoryTheory.GrothendieckTopology.Cover.Arrow.middle {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.bind S T)) : 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

• CategoryTheory.GrothendieckTopology.Cover.Arrow.middle I = Exists.choose ⋯

noncomputable def CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.bind S T)) : I.Y ⟶ CategoryTheory.GrothendieckTopology.Cover.Arrow.middle I

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

• CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom I = Exists.choose ⋯

noncomputable def CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.bind S T)) : CategoryTheory.GrothendieckTopology.Cover.Arrow.middle I ⟶ 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

• CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom I = Exists.choose ⋯

theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.from_middle_condition {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.bind S T)) : (CategoryTheory.GrothendieckTopology.Cover.sieve S).arrows (CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom I)

noncomputable def CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddle {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.bind S T)) : CategoryTheory.GrothendieckTopology.Cover.Arrow S

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

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

theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.to_middle_condition {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.bind S T)) : (CategoryTheory.GrothendieckTopology.Cover.sieve (T (CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddle I))).arrows (CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom I)

noncomputable def CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddle {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.bind S T)) : CategoryTheory.GrothendieckTopology.Cover.Arrow (T (CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddle I))

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

• CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddle I = { Y := I.Y, f := CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom I, hf := ⋯ }

theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C} {S : CategoryTheory.GrothendieckTopology.Cover J X} {T : (I : CategoryTheory.GrothendieckTopology.Cover.Arrow S) → CategoryTheory.GrothendieckTopology.Cover J I.Y} (I : CategoryTheory.GrothendieckTopology.Cover.Arrow (CategoryTheory.GrothendieckTopology.Cover.bind S T)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddleHom I) (CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom I) = I.f

def CategoryTheory.GrothendieckTopology.Cover.index {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (S : CategoryTheory.GrothendieckTopology.Cover J X) (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Limits.MulticospanIndex D

To every S : J.Cover X and presheaf P, associate a MulticospanIndex.

Equations

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

@[inline, reducible]

abbrev CategoryTheory.GrothendieckTopology.Cover.multifork {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (S : CategoryTheory.GrothendieckTopology.Cover J X) (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index S 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.

Equations

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

@[inline, reducible]

noncomputable abbrev CategoryTheory.GrothendieckTopology.Cover.toMultiequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (S : CategoryTheory.GrothendieckTopology.Cover J X) (P : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] : P.obj (Opposite.op X) ⟶ CategoryTheory.Limits.multiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S 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.

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.pullback_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) (S : CategoryTheory.GrothendieckTopology.Cover J X) : (CategoryTheory.GrothendieckTopology.pullback J f).obj S = CategoryTheory.GrothendieckTopology.Cover.pullback S f

def CategoryTheory.GrothendieckTopology.pullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X) : CategoryTheory.Functor (CategoryTheory.GrothendieckTopology.Cover J X) (CategoryTheory.GrothendieckTopology.Cover J Y)

Pull back a cover along a morphism.

Equations

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

def CategoryTheory.GrothendieckTopology.pullbackId {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : CategoryTheory.GrothendieckTopology.pullback J (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (CategoryTheory.GrothendieckTopology.Cover J X)

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

Equations

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

def CategoryTheory.GrothendieckTopology.pullbackComp {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.GrothendieckTopology.pullback J (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.pullback J g) (CategoryTheory.GrothendieckTopology.pullback J f)

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

Equations

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