Sites on P.Over ⊤ X

We provide some API for proving properties of P.Over ⊤ X in relation to precoverages. Consider a precoverage K on C.

Main results

• CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le: The forgetful functor P.Over ⊤ X ⥤ Over X is locally cover dense if morphisms in K satisfy P.
• CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_restrictedTopology: The topology generated by the precoverage induced from K via the composition P.Over ⊤ X ⥤ Over X ⥤ C is the induced topology from the forgetful functor P.Over ⊤ X ⥤ Over X.

theorem CategoryTheory.MorphismProperty.exists_map_eq_of_presieve {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} {S : C} [P.IsStableUnderComposition] (K : Precoverage C) (H : K ≤ P.precoverage) {X : P.Over ⊤ S} {R : Presieve ((Over.forget P ⊤ S).obj X)} (hR : R ∈ (Precoverage.comap (CategoryTheory.Over.forget S) K).coverings ((Over.forget P ⊤ S).obj X)) : ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = R

theorem CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} {S : C} [P.IsStableUnderComposition] (K : Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] (H : K ≤ P.precoverage) : (Over.forget P ⊤ S).LocallyCoverDense (K.toGrothendieck.over S)

theorem CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_restrictedTopology {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} {S : C} [P.IsStableUnderComposition] (K : Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] (H : K ≤ P.precoverage) : (Precoverage.comap ((Over.forget P ⊤ S).comp (CategoryTheory.Over.forget S)) K).toGrothendieck = (Over.forget P ⊤ S).restrictedTopology (K.toGrothendieck.over S)

theorem CategoryTheory.MorphismProperty.coverPreserving_comap_forget {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} {S : C} [P.IsStableUnderComposition] (K : Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] (H : K ≤ P.precoverage) : CoverPreserving (Precoverage.comap ((Over.forget P ⊤ S).comp (CategoryTheory.Over.forget S)) K).toGrothendieck (K.toGrothendieck.over S) (Over.forget P ⊤ S)

theorem CategoryTheory.MorphismProperty.isContinuous_comap_forget {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} {S : C} [P.IsStableUnderComposition] (K : Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] [Limits.HasFiniteWidePullbacks C] [P.HasOfPostcompProperty P] [P.IsStableUnderBaseChange] [P.ContainsIdentities] (H : K ≤ P.precoverage) : (Over.forget P ⊤ S).IsContinuous (Precoverage.comap ((Over.forget P ⊤ S).comp (CategoryTheory.Over.forget S)) K).toGrothendieck (K.toGrothendieck.over S)

theorem CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} {S : C} [P.IsStableUnderComposition] (K : Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] [Limits.HasFiniteWidePullbacks C] [P.HasOfPostcompProperty P] [P.IsStableUnderBaseChange] [P.ContainsIdentities] (H : K ≤ P.precoverage) : (Precoverage.comap ((Over.forget P ⊤ S).comp (CategoryTheory.Over.forget S)) K).toGrothendieck = (Over.forget P ⊤ S).inducedTopology (K.toGrothendieck.over S)