amalgamate_map — Mathlib

English

A technical lemma ensuring that amalgamation is compatible with P.map cones, i.e., glueing commutes with map on arrows.

Русский

Теорема о совместимости амальгаммации с отображениями P.map, т.е. склейка совместима с отображениями стрелок.

LaTeX

$$$hP.amalgamate S x hx ≫ P.map I.f.op = x I.f$$$

Lean4

@[reassoc (attr := simp)]
theorem amalgamate_map {A : Type u₂} [Category.{v₂} A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A} (hP : Presheaf.IsSheaf J P)
    (S : J.Cover X) (x : ∀ I : S.Arrow, E ⟶ P.obj (op I.Y))
    (hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), x I₁ ≫ P.map r.g₁.op = x I₂ ≫ P.map r.g₂.op) (I : S.Arrow) :
    hP.amalgamate S x hx ≫ P.map I.f.op = x _ := by apply (hP _ _ S.condition).valid_glue

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