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.

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

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

Equations

• CategoryTheory.Types.jointlySurjectivePrecoverage = { coverings := fun (X : Type ?u.9) (R : CategoryTheory.Presieve X) => ∀ (x : X), ∃ (Y : Type ?u.9) (g : Y ⟶ X), R g ∧ x ∈ Set.range g }

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 g

theorem CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iff {X Y : Type u} {f : X ⟶ Y} : Presieve.singleton f ∈ jointlySurjectivePrecoverage.coverings Y ↔ Function.Surjective f

@[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 : X), ∃ (i : ι), x ∈ Set.range (f i)

instance CategoryTheory.Types.instHasIsosJointlySurjectivePrecoverage : jointlySurjectivePrecoverage.HasIsos

instance CategoryTheory.Types.instIsStableUnderCompositionJointlySurjectivePrecoverage : jointlySurjectivePrecoverage.IsStableUnderComposition

instance CategoryTheory.Types.instIsStableUnderSupJointlySurjectivePrecoverage : jointlySurjectivePrecoverage.IsStableUnderSup

theorem CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff {C : Type u_1} [Category.{u_2, 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 (F.map f)

theorem CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff {C : Type u_1} [Category.{u_3, 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 (F.map (f i))

theorem CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage {C : Type u_1} [Category.{u_2, 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 (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.

instance CategoryTheory.instIsStableUnderBaseChangeJointlySurjectivePrecoverage : Types.jointlySurjectivePrecoverage.IsStableUnderBaseChange