sep — Mathlib

English

The presheaf P⁺ is separated: if two sections over a cover become equal when pulled back along all arrows of a cover, then the two sections are equal.

Русский

Прешефф P⁺ разложим: если две секции над покрытием становятся равными после тягивания по всем стрелкам покрытия, то сами секции равны.

LaTeX

$$$P^+\\;\\text{separated: }\\forall X,S, x,y\\in ToType((J.plusObj P).obj(op X)),\\; (\\forall I:S.Arrow,\\; P.map I.f.op x = P.map I.f.op y) \\Rightarrow x=y$$$

Lean4

/-- `P⁺` is always separated. -/
theorem sep {X : C} (P : Cᵒᵖ ⥤ D) (S : J.Cover X) (x y : ToType ((J.plusObj P).obj (op X)))
    (h : ∀ I : S.Arrow, (J.plusObj P).map I.f.op x = (J.plusObj P).map I.f.op y) : x = y := by
  -- First, we choose representatives for x and y.

  obtain ⟨Sx, x, rfl⟩ := exists_rep x
  obtain ⟨Sy, y, rfl⟩ := exists_rep y
  simp only [res_mk_eq_mk_pullback] at h
  choose W h1 h2 hh using fun I : S.Arrow =>
    (eq_mk_iff_exists _ _).mp
      (h I)
        -- To prove equality, it suffices to prove that there exists a cover over which
          -- the representatives become equal.

  rw [eq_mk_iff_exists]
    -- Construct the cover over which the representatives become equal by combining the various
      -- covers chosen above.

  let B : J.Cover X := S.bind W
  use B
  let ex : B ⟶ Sx :=
    homOfLE
      (by
        rintro Y f ⟨Z, e1, e2, he2, he1, hee⟩
        rw [← hee]
        apply leOfHom (h1 ⟨_, _, he2⟩)
        exact he1)
  let ey : B ⟶ Sy :=
    homOfLE
      (by
        rintro Y f ⟨Z, e1, e2, he2, he1, hee⟩
        rw [← hee]
        apply leOfHom (h2 ⟨_, _, he2⟩)
        exact he1)
  use ex, ey
  ext1 I
  let IS : S.Arrow := I.fromMiddle
  specialize hh IS
  let IW : (W IS).Arrow := I.toMiddle
  apply_fun fun e => e IW at hh
  convert hh using 1
  · exact x.congr_apply I.middle_spec.symm _
  · exact y.congr_apply I.middle_spec.symm _

Похожие утверждения