Documentation

Mathlib.CategoryTheory.Sites.JointlySurjective

The jointly surjective precoverage #

In the category of types, the jointly surjective precoverage has the jointly surjective families as coverings. We show that this precoverage is stable under the standard constructions.

Notes #

See Mathlib/CategoryTheory/Sites/Types.lean for the Grothendieck topology of jointly surjective covers.

source
def CategoryTheory.Types.jointlySurjectivePrecoverage :
Precoverage (Type u)

The jointly surjective precoverage in the category of types has the jointly surjective families as coverings.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.Types.mem_jointlySurjectivePrecoverage_iff {X : Type u} {R : Presieve X} :
    R ∈ jointlySurjectivePrecoverage.coverings X ↔ ∀ (x : X), ∃ (Y : Type u) (g : Y ⟶ X), R g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)
    source
    theorem CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iff {X Y : Type u} {f : X ⟶ Y} :
    Presieve.singleton f ∈ jointlySurjectivePrecoverage.coverings Y ↔ Function.Surjective ⇑(ConcreteCategory.hom f)
    source
    @[simp]
    theorem CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff {X : Type u} {ι : Type u_1} {Y : ι → Type u} {f : (i : ι) → Y i ⟶ X} :
    Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X ↔ ∀ (x : (fun (X : Type u) => X) X), ∃ (i : ι), x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
    source
    instance CategoryTheory.Types.instHasIsosJointlySurjectivePrecoverage :
    jointlySurjectivePrecoverage.HasIsos
    source
    instance CategoryTheory.Types.instIsStableUnderCompositionJointlySurjectivePrecoverage :
    jointlySurjectivePrecoverage.IsStableUnderComposition
    source
    instance CategoryTheory.Types.instIsStableUnderSupJointlySurjectivePrecoverage :
    jointlySurjectivePrecoverage.IsStableUnderSup
    source
    instance CategoryTheory.Types.instSmallJointlySurjectivePrecoverage :
    jointlySurjectivePrecoverage.Small
    source
    theorem CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C (Type u)) {X : C} {R : Presieve X} :
    R ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings X ↔ ∀ (x : F.obj X), ∃ (Y : C) (f : Y ⟶ X), R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map f))
    source
    theorem CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C (Type u)) {X : C} {ι : Type u_2} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} :
    ofArrows Y f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings X ↔ ∀ (x : F.obj X), ∃ (i : ι), x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
    source
    theorem CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage {C : Type u_1} [Category.{v_1, u_1} C] (F : Functor C (Type u)) (H : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : Limits.HasPullback f g], Function.Surjective ⇑(ConcreteCategory.hom (Limits.pullbackComparison F f g))) :
    (Precoverage.comap F Types.jointlySurjectivePrecoverage).IsStableUnderBaseChange

    The pullback of the jointly surjective precoverage of types to any category C via a (forgetful) functor C ⥤ Type u is stable under base change if the canonical map F (X ×[Y] Z) ⟶ F(X) ×[F(Y)] F(Z) is surjective.

    source
    instance CategoryTheory.instIsStableUnderBaseChangeJointlySurjectivePrecoverage :
    Types.jointlySurjectivePrecoverage.IsStableUnderBaseChange