pullbackConeOfLeftFst — Mathlib

English

A natural compatibility between invApp and f.c.app on an open U.

Русский

Естественная совместимость между invApp и f.c.app на открытом U.

LaTeX

$$invApp f U ≫ f.c.app (op (opensFunctor f |>.obj U)) = Y.presheaf.map (homOfLE (...)).op$$

Lean4

/-- (Implementation.) The projection map when constructing the pullback along an open immersion.
-/
def pullbackConeOfLeftFst : Y.restrict (TopCat.snd_isOpenEmbedding_of_left hf.base_open g.base) ⟶ X
    where
  base := pullback.fst _ _
  c :=
    { app := fun U =>
        hf.invApp _ (unop U) ≫
          g.c.app (op (hf.base_open.isOpenMap.functor.obj (unop U))) ≫
            Y.presheaf.map
              (eqToHom
                (by
                  simp only [IsOpenMap.functor, op_inj_iff, Opens.map, Functor.op_obj]
                  apply LE.le.antisymm
                  · rintro _ ⟨_, h₁, h₂⟩
                    use
                      (TopCat.pullbackIsoProdSubtype _ _).inv
                        ⟨⟨_, _⟩, h₂⟩
                          -- Porting note: used to be `simpa using h₁`

                    simp only [restrict_carrier, Opens.coe_mk, Set.mem_preimage, SetLike.mem_coe]
                      -- The next `rw` can't be done by `simp`, but `restrict_carrier` can't be used
                                          -- by `rw`.

                    rw [TopCat.pullbackIsoProdSubtype_inv_fst_apply, TopCat.pullbackIsoProdSubtype_inv_snd_apply]
                    simpa using h₁
                  · rintro _ ⟨x, h₁, rfl⟩
                    exact ⟨_, h₁, CategoryTheory.congr_fun pullback.condition x⟩))
      naturality := by
        intro U V i
        induction U
        induction V
        rw [inv_naturality_assoc]
        dsimp
        simp only [NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_map, Quiver.Hom.unop_op,
          ← Functor.map_comp, Category.assoc]
        rfl }

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