sections_ext — Mathlib

English

The extensionality principle for CoversTop: if a cover Y induces equality of components, then the arrows themselves are equal.

Русский

Принцип эктенсиональности для CoversTop: если покрытие Y порождает равенство компонент, то отображения сами равны.

LaTeX

$$$\\forall F:\\\n \\text{CoversTop } Y \\Rightarrow\\forall f,g:\\; X\\to c.pt,\\ (\\forall i, f\\circ \\pi_{Y_i}=g\\circ\\pi_{Y_i})\\Rightarrow f=g$$$

Lean4

theorem sections_ext (F : Sheaf J (Type _)) {x y : F.1.sections}
    (h : ∀ (i : I), x.1 (Opposite.op (Y i)) = y.1 (Opposite.op (Y i))) : x = y :=
  by
  ext W
  apply (((isSheaf_iff_isSheaf_of_type _ _).1 F.2).isSeparated _ (hY W.unop)).ext
  rintro T a ⟨i, ⟨b⟩⟩
  simpa using congr_arg (F.1.map b.op) (h i)

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