Γ_Spec_left_triangle — Mathlib

English

The left triangle identity is satisfied for the canonical morphisms in the Γ-Spec adjunction.

Русский

Левая треугольная тождественность выполняется для канонических морфизмов сопряжения.

LaTeX

$$Γ_Spec_left_triangle_part := ...$$

Lean4

/-- `toSpecΓ _` is an isomorphism so these are mutually two-sided inverses. -/
theorem Γ_Spec_left_triangle : toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 _ :=
  by
  unfold toSpecΓ
  rw [← toOpen_res _ (basicOpen (1 : Γ.obj (op X))) ⊤ (eqToHom basicOpen_one.symm), Category.assoc, NatTrans.naturality,
    ← Category.assoc]
  erw [X.toΓSpecSheafedSpace_app_spec 1, ← Functor.map_comp]
  convert eqToHom_map X.presheaf _; rfl

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