inter — Mathlib

Lean4
/-- Intersection of two `1`-hypercovers. -/
@[simps toPreOneHypercover]
noncomputable def inter [HasPullbacks C] (E F : J.OneHypercover S)
    [∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)]
    [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)] :
    J.OneHypercover S where
  __ := E.toPreOneHypercover.inter F.toPreOneHypercover
  mem₀ := (E.toZeroHypercover.inter F.toZeroHypercover).mem₀
  mem₁ i₁ i₂ W p₁ p₂
    h := by
    rw [PreOneHypercover.sieve₁_inter h]
    refine J.bind_covering (E.mem₁ _ _ _ _ (by simpa using h)) fun _ _ _ ↦ ?_
    exact J.pullback_stable _ (F.mem₁ _ _ _ _ (by simpa [Category.assoc, ← pullback.condition]))
Похожие утверждения