Lean4
/-- The pullback of a cover of `S`-schemes with `Q` along a morphism of `S`-schemes. This is not
definitionally equal to `AlgebraicGeometry.Scheme.Cover.pullbackCover`, as here we take
the pullback in `Q.Over ⊤ S`, whose underlying scheme is only isomorphic but not equal to the
pullback in `Scheme`. -/
@[simps -isSimp]
def pullbackCoverOverProp : W.Cover (precoverage P)
where
I₀ := 𝒰.I₀
X x := (pullback (f.asOverProp (hX := hW) (hY := hX) S) ((𝒰.f x).asOverProp (hX := hQ x) (hY := hX) S)).left
f x := (pullback.fst (f.asOverProp S) ((𝒰.f x).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_fst _ _ _) 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_fst, P.cancel_left_of_respectsIso]
exact P.pullback_fst _ _ (𝒰.map_prop j)
