English
In the Type universe, the comap of jointlySurjectivePrecoverage is stable under base change.
Русский
В универсе типов комап jointlySurjectivePrecoverage устойчив к базовому изменению.
LaTeX
$$isStableUnderBaseChange_comap_jointlySurjectivePrecoverage$$
Lean4
/-- 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. -/
theorem isStableUnderBaseChange_comap_jointlySurjectivePrecoverage
(H : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [HasPullback f g], Function.Surjective (pullbackComparison F f g)) :
(Types.jointlySurjectivePrecoverage.comap F).IsStableUnderBaseChange where
mem_coverings_of_isPullback {ι} S X f hf Y g P p₁ p₂
h :=
by
rw [Precoverage.mem_comap_iff, Presieve.map_ofArrows, Types.ofArrows_mem_jointlySurjectivePrecoverage_iff] at hf ⊢
intro x
obtain ⟨i, hi⟩ := hf (F.map g x)
have : HasPullback g (f i) := (h i).hasPullback
use i
have : F.map (p₁ i) = F.map ((h i).isoPullback.hom) ≫ pullbackComparison F g (f i) ≫ pullback.fst _ _ := by
simp [← Functor.map_comp]
rwa [this, types_comp, types_comp, Function.comp_assoc, Set.range_comp,
Function.Surjective.range_eq <| (H _ _).comp (surjective_of_epi _), Set.image_univ, Types.range_pullbackFst]
