CategoryTheory.EffectiveEpiFamily.transitive_of_finite
theorem CategoryTheory.EffectiveEpiFamily.transitive_of_finite :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Precoherent C] {X : C}
{α : Type} [inst_2 : Finite α] {Y : α → C} (π : (a : α) → Y a ⟶ X),
CategoryTheory.EffectiveEpiFamily Y π →
∀ {β : α → Type} [inst_3 : ∀ (a : α), Finite (β a)] {Y_n : (a : α) → β a → C}
(π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a),
(∀ (a : α), CategoryTheory.EffectiveEpiFamily (Y_n a) (π_n a)) →
CategoryTheory.EffectiveEpiFamily (fun c => Y_n c.fst c.snd) fun c =>
CategoryTheory.CategoryStruct.comp (π_n c.fst c.snd) (π c.fst)
This theorem states that in a precoherent category, the property of being an effective epimorphic family is transitive. Specifically, if we have an effective epi family indexed by some set $\alpha$ (denoted as `EffectiveEpiFamily Y π`), and for each member `a` in this set, we have another effective epi family indexed by some set `β a` (denoted as `EffectiveEpiFamily (Y_n a) (π_n a)`), then the composition (using the category's composition operation `CategoryTheory.CategoryStruct.comp`) also forms an effective epi family.
The theorem also notes that the finiteness condition on the index sets is likely an artifact of the proof, suggesting that this condition might not be necessary for the property to hold.
More concisely: In a precoherent category, if every member of an effective epimorphic family has an effective epimorphic family indexed by some set, then the composition of these families is an effective epimorphic family.
|
CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily
theorem CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Precoherent C] {X : C}
(S : CategoryTheory.Sieve X),
S ∈ (CategoryTheory.coherentTopology C).sieves X ↔
∃ α, ∃ (_ : Finite α), ∃ Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
This theorem states that in a precoherent category `C`, a sieve `S` over an object `X` belongs to the coherent Grothendieck topology of `C` if and only if there exists a finite effective epimorphic family `π` indexed by `α` with codomain `Y`, such that every morphism in this family is an arrow of the sieve `S`.
More concisely: In a precoherent category, a sieve over an object belongs to its coherent Grothendieck topology if and only if there exists a finite, effective epimorphic family with codomain some object and whose morphisms are all in the sieve.
|
CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily
theorem CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Precoherent C] {X : C}
(S : CategoryTheory.Sieve X),
(∃ α, ∃ (_ : Finite α), ∃ Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
S ∈ (CategoryTheory.coherentTopology C).sieves X
This theorem states that in a precoherent category, any sieve that contains an 'EffectiveEpiFamily' is a sieve of the coherent topology. Given a category and an object in this category, if there exists a finite index set along with a family of morphisms and an object such that this family forms an 'EffectiveEpiFamily', and every morphism in this family is a member of the given sieve's arrows, then the sieve is a member of the sieves of the coherent topology generated by the category at the given object. Note that this is one direction of a larger theorem (`mem_sieves_iff_hasEffectiveEpiFamily`), but this part is needed for the proof of the larger theorem.
More concisely: In a precoherent category, a sieve containing an EffectiveEpiFamily is a sieve of the coherent topology.
|