sheaf_eq_amalgamation — Mathlib

English

A sheaf condition equates amalgamations with glueings inside the condensed structure given by the cond.

Русский

Условия sheaf приводят равенство амальгамаций и склейок внутри конденсированной структуры, определяемой cond.

LaTeX

$$$\\text{Amalgamation} = (\\mathcal F.cond X T h_T).amalgamate$$$

Lean4

theorem sheaf_eq_amalgamation (ℱ : Sheaf K A) {X : A} {U : D} {T : Sieve U} (hT) (x : FamilyOfElements _ T) (hx) (t)
    (h : x.IsAmalgamation t) : t = (ℱ.cond X T hT).amalgamate x hx :=
  (ℱ.cond X T hT).isSeparatedFor x t _ h ((ℱ.cond X T hT).isAmalgamation hx)

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