The Finite Pretopology

In this file we define the finite pretopology on a category, which consists of presieves that contain only finitely many arrows.

Main Definitions

• CategoryTheory.Precoverage.finite: The finite precoverage on a category.
• CategoryTheory.Pretopology.finite: The finite pretopology on a category.

def CategoryTheory.Precoverage.finite (C : Type u) [Category.{v, u} C] : Precoverage C

The finite precoverage on a category consists of finite presieves, i.e. a presieve with finitely many maps after uncurrying.

Equations

• CategoryTheory.Precoverage.finite C = { coverings := fun (X : C) => {s : CategoryTheory.Presieve X | s.uncurry.Finite} }

@[simp]

theorem CategoryTheory.Precoverage.mem_finite_iff {C : Type u} [Category.{v, u} C] {X : C} {s : Presieve X} : s ∈ (finite C).coverings X ↔ s.uncurry.Finite

theorem CategoryTheory.Precoverage.ofArrows_mem_finite {C : Type u} [Category.{v, u} C] {X : C} {ι : Type u_1} [Finite ι] (Y : ι → C) (f : (i : ι) → Y i ⟶ X) : Presieve.ofArrows Y f ∈ (finite C).coverings X

instance CategoryTheory.Precoverage.instHasIsosFinite {C : Type u} [Category.{v, u} C] : (finite C).HasIsos

def CategoryTheory.Pretopology.finite (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : Pretopology C

The finite pretopology on a category consists of finite presieves, i.e. a presieve with finitely many maps after uncurrying.

Equations

• CategoryTheory.Pretopology.finite C = { toPrecoverage := CategoryTheory.Precoverage.finite C, has_isos := ⋯, pullbacks := ⋯, transitive := ⋯ }

@[simp]

theorem CategoryTheory.Pretopology.finite_toPrecoverage (C : Type u) [Category.{v, u} C] [Limits.HasPullbacks C] : (finite C).toPrecoverage = Precoverage.finite C

theorem CategoryTheory.Pretopology.ofArrows_mem_finite {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X : C} {ι : Type u_1} [Finite ι] (Y : ι → C) (f : (i : ι) → Y i ⟶ X) : Presieve.ofArrows Y f ∈ (finite C).coverings X