whiskerLeft_obj_map_bijective_of_isCoverDense

English

If G is cover-dense and full, then the map on Hom-sets induced by whiskering with G.op is bijective when Q is a sheaf.

Русский

Если G плотный по подслоям и полно, то отображение на множества гомоморфизмов, индуцированное whiskerLeft с G.op, биективно, когда Q — шейф.

LaTeX

$$$\text{Bijective}(((\mathrm{whiskeringLeft}\ C^{op}\ D^{op}\ A).op).map : (P \to Q) \to (G^{op} \circ P \to G^{op} \circ Q)).$$$

Lean4

/-- If `G : C ⥤ D` is cover dense and full, then the
map `(P ⟶ Q) → (G.op ⋙ P ⟶ G.op ⋙ Q)` is bijective when `Q` is a sheaf`. -/
theorem whiskerLeft_obj_map_bijective_of_isCoverDense (G : C ⥤ D) [G.IsCoverDense K] [G.IsLocallyFull K] {A : Type*}
    [Category A] (P Q : Dᵒᵖ ⥤ A) (hQ : Presheaf.IsSheaf K Q) :
    Function.Bijective (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map : (P ⟶ Q) → _) :=
  (IsCoverDense.restrictHomEquivHom (ℱ' := ⟨Q, hQ⟩)).symm.bijective

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