Lean4
/-- A variant of `AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp` with the arguments in the
fiber products flipped. -/
@[simps -isSimp]
def pullbackCoverOverProp' : W.Cover (precoverage P)
where
I₀ := 𝒰.I₀
X x := (pullback ((𝒰.f x).asOverProp (hX := hQ x) (hY := hX) S) (f.asOverProp (hX := hW) (hY := hX) S)).left
f x := (pullback.snd ((𝒰.f x).asOverProp S) (f.asOverProp S)).left
mem₀ := by
rw [presieve₀_mem_precoverage_iff]
refine ⟨fun x ↦ ?_, fun j ↦ ?_⟩
· obtain ⟨i, hy⟩ := Cover.exists_eq (𝒰.pullback₂ f) x
use i
exact
(mem_range_iff_of_surjective ((𝒰.pullback₂ f).f i) _
((PreservesPullback.iso (MorphismProperty.Over.forget Q _ _ ⋙ Over.forget S) ((𝒰.f _).asOverProp S)
(f.asOverProp S)).inv)
(PreservesPullback.iso_inv_snd _ _ _) x).mp
hy
· dsimp only
rw [← Over.forget_map, MorphismProperty.Comma.toCommaMorphism_eq_hom, ← MorphismProperty.Comma.forget_map, ←
Functor.comp_map]
rw [← PreservesPullback.iso_hom_snd, P.cancel_left_of_respectsIso]
exact P.pullback_snd _ _ (𝒰.map_prop j)
