English
A simplification lemma about base change stability for the jointly surjective preserving precoverage.
Русский
Лемма упрощения о стабильности под базовым изменением для предпокрытия, сохраняющего совместную сюръективность.
LaTeX
$$instance [IsJointlySurjectivePreserving P] [P.IsStableUnderBaseChange] : (precoverage P).IsStableUnderBaseChange$$
Lean4
instance [IsJointlySurjectivePreserving P] [P.IsStableUnderBaseChange] : (precoverage P).IsStableUnderBaseChange where
mem_coverings_of_isPullback {ι} S X f hf Y g T p₁ p₂
H := by
rw [ofArrows_mem_precoverage_iff] at hf ⊢
refine ⟨fun x ↦ ?_, fun i ↦ P.of_isPullback (H i).flip (hf.2 i)⟩
obtain ⟨i, y, hy⟩ := hf.1 (g.base x)
have := (H i).hasPullback
obtain ⟨w, hw⟩ := IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop (hf.2 i) (f := g) x y hy.symm
use i, (H i).isoPullback.inv.base w
simpa [← Scheme.comp_base_apply]
