to_sheafify_lift_unique — Mathlib

English

If two lifts l1 and l2 from G.sheafify to F' become equal after composing with the same morphism e, then l1 = l2.

Русский

Если два лифта l1 и l2 из G.sheafify в F' совпадают после композиции с одним и тем же морфизмом e, то l1 = l2.

LaTeX

$$$ l_1 = l_2 $ if $ e : Subpresheaf.homOfLe (G.le_sheafify J) \\circ l_1 = Subpresheaf.homOfLe (G.le_sheafify J) \\circ l_2 $$$

Lean4

theorem to_sheafify_lift_unique (h : Presieve.IsSheaf J F') (l₁ l₂ : (G.sheafify J).toPresheaf ⟶ F')
    (e : Subpresheaf.homOfLe (G.le_sheafify J) ≫ l₁ = Subpresheaf.homOfLe (G.le_sheafify J) ≫ l₂) : l₁ = l₂ :=
  by
  ext U ⟨s, hs⟩
  apply (h _ hs).isSeparatedFor.ext
  rintro V i hi
  dsimp at hi
  rw [← FunctorToTypes.naturality, ← FunctorToTypes.naturality]
  exact (congr_fun (congr_app e <| op V) ⟨_, hi⟩ :)

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