intersectionOfLocallyDirected — Mathlib

Lean4
/-- If `𝒰` is a directed cover of `X`, this is the cover of `𝒰ᵢ ×[X] 𝒰ⱼ` by `{𝒰ₖ}` where
`k ≤ i` and `k ≤ j`. -/
@[simps f]
def intersectionOfLocallyDirected [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] (i j : 𝒰.I₀) :
    (pullback (𝒰.f i) (𝒰.f j)).Cover (precoverage P)
    where
  I₀ := Σ (k : 𝒰.I₀), (k ⟶ i) × (k ⟶ j)
  X k := 𝒰.X k.1
  f k := pullback.lift (𝒰.trans k.2.1) (𝒰.trans k.2.2) (by simp)
  mem₀ := by
    rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun k ↦ ?_⟩
    · use
        ⟨(𝒰.exists_lift_trans_eq x).choose, (𝒰.exists_lift_trans_eq x).choose_spec.choose,
          (𝒰.exists_lift_trans_eq x).choose_spec.choose_spec.choose⟩
      exact (𝒰.exists_lift_trans_eq x).choose_spec.choose_spec.choose_spec
    · apply P.of_postcomp (W' := P) _ (pullback.fst _ _) (P.pullback_fst _ _ (𝒰.map_prop _))
      rw [pullback.lift_fst]
      exact 𝒰.property_trans _
Похожие утверждения