pullbackCoverOver' — Mathlib

Lean4
/-- A variant of `AlgebraicGeometry.Scheme.Cover.pullbackCoverOver` with the arguments in the
fiber products flipped. -/
@[simps]
def pullbackCoverOver' : W.Cover (precoverage P) where
  I₀ := 𝒰.I₀
  X x := (pullback ((𝒰.f x).asOver S) (f.asOver S)).left
  f x := (pullback.snd ((𝒰.f x).asOver S) (f.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 _) _
              ((PreservesPullback.iso (Over.forget S) ((𝒰.f _).asOver S) (f.asOver S)).inv)
              (PreservesPullback.iso_inv_snd _ _ _) x).mp
          hy
    · dsimp only
      rw [← Over.forget_map, ← PreservesPullback.iso_hom_snd, P.cancel_left_of_respectsIso]
      exact P.pullback_snd _ _ (𝒰.map_prop j)
Похожие утверждения