isIso — Mathlib

English

Let X, Y be presheafed spaces and α : X ⟶ Y. For x, x' ∈ X with h : x = x', one has α.stalkMap x ≫ eqToHom (X.presheaf.stalk x = X.presheaf.stalk x') = eqToHom (Y.presheaf.stalk (α.base x) = Y.presheaf.stalk (α.base x')) ≫ α.stalkMap x'.

Русский

Пусть X, Y — предшаблонные пространства и α : X ⟶ Y. Для точек x, x' ∈ X с h : x = x' выполняется α.stalkMap x ≫ eqToHom (X.presheaf.stalk x = X.presheaf.stalk x') = eqToHom (Y.presheaf.stalk (α.base x) = Y.presheaf.stalk (α.base x')) ≫ α.stalkMap x'.

LaTeX

$$$$\\alpha.stalkMap x \\;\\; \\;\\; \\; = \\;\\; \\mathrm{eqToHom}\\Big( X.presheaf.stalk x = X.presheaf.stalk x' \\Big) \\; \\; ≫ \\;\\; \\alpha.stalkMap x' $$$$

Lean4

instance isIso {X Y : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) [IsIso α] (x : X) : IsIso (α.stalkMap x) where
  out := by
    let β : Y ⟶ X := CategoryTheory.inv α
    have h_eq : (α ≫ β).base x = x := by
      rw [IsIso.hom_inv_id α, id_base, TopCat.id_app]
        -- Intuitively, the inverse of the stalk map of `α` at `x` should just be the stalk map of `β`
            -- at `α x`. Unfortunately, we have a problem with dependent type theory here: Because `x`
            -- is not *definitionally* equal to `β (α x)`, the map `stalk_map β (α x)` has not the correct
            -- type for an inverse.
            -- To get a proper inverse, we need to compose with the `eqToHom` arrow
            -- `X.stalk x ⟶ X.stalk ((α ≫ β).base x)`.

    refine
      ⟨eqToHom (show X.presheaf.stalk x = X.presheaf.stalk ((α ≫ β).base x) by rw [h_eq]) ≫ (β.stalkMap (α.base x) :),
        ?_, ?_⟩
    · rw [← Category.assoc, congr_point α x ((α ≫ β).base x) h_eq.symm, Category.assoc]
      erw [← stalkMap.comp β α (α.base x)]
      rw [congr_hom _ _ (IsIso.inv_hom_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]
    ·
      rw [Category.assoc, ← stalkMap.comp, congr_hom _ _ (IsIso.hom_inv_id α), stalkMap.id, eqToHom_trans_assoc,
        eqToHom_refl, Category.id_comp]

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