f_invApp_f_app — Mathlib

English

There exists an equality witnessing the commutativity of a square formed by invApp and t_app in the gluing data; i.e., a witness eq such that a composed path equals another path in the diagram.

Русский

Существет свидетельство равенства, фиксирующее равносильность квадратов в данных склейки; существует eq, чтобы композиции путей совпадали.

LaTeX

$$$\\exists eq:\\; (π_2^{-1} i,j,k)U \\;\\text{and related arrows commute with } D.t_k i \\text{ and } D.t'\\,k i j$$$

Lean4

/-- The red and the blue arrows in ![this diagram](https://i.imgur.com/0GiBUh6.png) commute. -/
@[simp, reassoc]
theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) :
    (D.f_open i j).invApp _ U ≫ (D.f i k).c.app _ =
      (π₁ i, j, k).c.app (op U) ≫
        (π₂⁻¹ i, j, k) (unop _) ≫
          (D.V _).presheaf.map
            (eqToHom
              (by
                delta IsOpenImmersion.opensFunctor
                dsimp only [Functor.op, IsOpenMap.functor, Opens.map, unop_op]
                congr
                apply pullback_base)) :=
  by
  have := PresheafedSpace.congr_app (@pullback.condition _ _ _ _ _ (D.f i j) (D.f i k) _)
  dsimp only [comp_c_app] at this
  rw [← cancel_epi (inv ((D.f_open i j).invApp _ U)), IsIso.inv_hom_id_assoc, IsOpenImmersion.inv_invApp]
  simp_rw [Category.assoc]
  erw [(π₁ i, j, k).c.naturality_assoc, reassoc_of% this, ← Functor.map_comp_assoc,
    IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc, ← (D.V (i, k)).presheaf.map_comp, ←
    (D.V (i, k)).presheaf.map_comp]
  convert (Category.comp_id _).symm
  erw [(D.V (i, k)).presheaf.map_id]
  rfl

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