Theorems · Theorem · category theory

CategoryTheory.extensive_regular_generate_coherent

∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryPreExtensive C],
  (CategoryTheory.extensiveCoverage C ⊔ CategoryTheory.regularCoverage C).toGrothendieck =
    CategoryTheory.coherentTopology C

The union of the extensive and regular coverages generates the coherent topology on C.

Defined in

Mathlib.CategoryTheory.Sites.Coherent.Comparison

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreregularCategoryTheory.FinitaryPreExtensive