Results on morphism properties

Results on morphism properties that should go into Mathlib.CategoryTheory.Sites.MorphismProperty or earlier files.

def CategoryTheory.MorphismProperty.toPresieveOn {C : Type u_1} [Category.{u_2, u_1} C] (P : MorphismProperty C) (X : C) : Presieve X

The presieve on X consisting of all morphisms to X that satisfy the property P.

Equations

• P.toPresieveOn X f = P f

def CategoryTheory.MorphismProperty.toSieveOn {C : Type u_1} [Category.{u_2, u_1} C] (P : MorphismProperty C) (X : C) : Sieve X

The sieve on X that is generated by P.toPresieve X, consisting of all morphisms that factor through a morphism satisfying P.

Equations

• P.toSieveOn X = CategoryTheory.Sieve.generate (P.toPresieveOn X)

@[simp]

theorem CategoryTheory.MorphismProperty.toSieveOn_apply {C : Type u_1} [Category.{u_2, u_1} C] (P : MorphismProperty C) (X Z : C) (f : Z ⟶ X) : (P.toSieveOn X).arrows f = ∃ (Y : C) (h : Z ⟶ Y) (g : Y ⟶ X), P.toPresieveOn X g ∧ CategoryStruct.comp h g = f

theorem CategoryTheory.MorphismProperty.toSieveOn_arrows_eq_toPresieveOn {C : Type u_1} [Category.{u_2, u_1} C] {P : MorphismProperty C} [P.RespectsLeft ⊤] {X : C} : (P.toSieveOn X).arrows = P.toPresieveOn X

theorem CategoryTheory.MorphismProperty.toPresieveOn_le_iff {C : Type u_1} [Category.{u_2, u_1} C] {P : MorphismProperty C} {X : C} (S : Presieve X) : P.toPresieveOn X ≤ S ↔ ∀ (Y : C) (f : Y ⟶ X), P f → S f

theorem CategoryTheory.MorphismProperty.toSieveOn_le_iff {C : Type u_1} [Category.{u_2, u_1} C] {P : MorphismProperty C} {X : C} (S : Sieve X) : P.toSieveOn X ≤ S ↔ ∀ (Y : C) (f : Y ⟶ X), P f → S.arrows f

class CategoryTheory.MorphismProperty.HasFactorizationInto {C : Type u_1} [Category.{u_2, u_1} C] (P Q Q' : MorphismProperty C) : Prop

Typeclass asserting that every morphism in P can be factored as a morphism in Q followed by a morphism in Q'.

• nonempty_mapFactorizationData ⦃X Y : C⦄ ⦃f : X ⟶ Y⦄ (hf : P f) : Nonempty (Q.MapFactorizationData Q' f)

def CategoryTheory.MorphismProperty.generatedTopology {C : Type u_1} [Category.{u_2, u_1} C] (P : MorphismProperty C) [P.RespectsRight ⊤] [P.HasFactorizationInto P P] : GrothendieckTopology C

For every morphism property P that is closed under composition with arbitrary morphisms from the right and has the property that every morphism in P can be factored into two morphisms in P, there exists a largest Grothendieck topology with the property that every morphism in P belongs to every covering sieve on its codomain. For the lack of an established name, we call this the Grothendieck topology generated by P.

Equations

• P.generatedTopology = { sieves := fun (X : C) (S : CategoryTheory.Sieve X) => P.toSieveOn X ≤ S, top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }

theorem CategoryTheory.MorphismProperty.le_generatedTopology_iff {C : Type u_1} [Category.{u_2, u_1} C] {P : MorphismProperty C} [P.RespectsRight ⊤] [P.HasFactorizationInto P P] (J : GrothendieckTopology C) : J ≤ P.generatedTopology ↔ ∀ (X : C), ∀ S ∈ J X, ∀ (Y : C) (f : Y ⟶ X), P f → S.arrows f

def CategoryTheory.MorphismProperty.morphismsThrough {C : Type u_1} [Category.{u_2, u_1} C] (X : C) : MorphismProperty C

The class of all morphisms that factor through X, as a MorphismProperty.

Equations

• CategoryTheory.MorphismProperty.morphismsThrough X f = ∃ (g : x✝¹ ⟶ X) (g' : X ⟶ x✝), CategoryTheory.CategoryStruct.comp g g' = f

instance CategoryTheory.MorphismProperty.instRespectsLeftMorphismsThroughTop {C : Type u_1} [Category.{u_2, u_1} C] {X : C} : (morphismsThrough X).RespectsLeft ⊤

instance CategoryTheory.MorphismProperty.instRespectsRightMorphismsThroughTop {C : Type u_1} [Category.{u_2, u_1} C] {X : C} : (morphismsThrough X).RespectsRight ⊤

instance CategoryTheory.MorphismProperty.instHasFactorizationIntoMorphismsThrough {C : Type u_1} [Category.{u_2, u_1} C] {X : C} : (morphismsThrough X).HasFactorizationInto (morphismsThrough X) (morphismsThrough X)