valid_glue — Mathlib

English

If t is an amalgamation for x, then P.map f.op (t.amalgamate x hx) = x f Hf for every arrow f with R f.

Русский

Если t является амальгаммой для x, тогда P.map f.op (t.amalgamate x hx) = x f Hf для каждого стрелки f, удовлетворяющего R.

LaTeX

$$valid_glue (t : IsSheafFor P R) {x} (hx) (f) (Hf) : P.map f.op (t.amalgamate x hx) = x f Hf$$

Lean4

@[simp]
theorem valid_glue (t : IsSheafFor P R) {x : FamilyOfElements P R} (hx : x.Compatible) (f : Y ⟶ X) (Hf : R f) :
    P.map f.op (t.amalgamate x hx) = x f Hf :=
  t.isAmalgamation hx f Hf

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