Lean4
/-- The pullback of a cover of `S`-schemes along a morphism of `S`-schemes. This is not
definitionally equal to `AlgebraicGeometry.Scheme.Cover.pullback₁`, as here we take
the pullback in `Over S`, whose underlying scheme is only isomorphic but not equal to the
pullback in `Scheme`. -/
@[simps]
def pullbackCoverOver : W.Cover (precoverage P) where
I₀ := 𝒰.I₀
X x := (pullback (f.asOver S) ((𝒰.f x).asOver S)).left
f x := (pullback.fst (f.asOver S) ((𝒰.f x).asOver 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 (Over.forget S) (f.asOver S) ((𝒰.f _).asOver S)).inv)
(PreservesPullback.iso_inv_fst _ _ _) x).mp
hy
· dsimp only
rw [← Over.forget_map, ← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]
exact P.pullback_fst _ _ (𝒰.map_prop j)
