isLocallySurjective_sheaf_of_types

English

For a preregular C and finitary PreExtensive C, a morphism of presheaves valued in Type is locally surjective iff it satisfies a type-level surjectivity condition.

Русский

Для прегрегулярной C и финитно-пре-extensive, морфизм презашифра в Type локально сюръективен тогда и только тогда, когда выполняется условие сюръективности на уровне типов.

LaTeX

$$$\mathrm{IsLocallySurjective}(f) \iff \forall X, \mathrm{Surjective}(f_X)$$$

Lean4

theorem isLocallySurjective_sheaf_of_types [Preregular C] [FinitaryPreExtensive C] {F G : Cᵒᵖ ⥤ Type w} (f : F ⟶ G)
    [PreservesFiniteProducts F] [PreservesFiniteProducts G] (h : Presheaf.IsLocallySurjective (coherentTopology C) f) :
    Presheaf.IsLocallySurjective (regularTopology C) f where
  imageSieve_mem
    y := by
    replace h := h.1 y
    rw [coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily] at h
    obtain ⟨α, _, Z, π, h, h'⟩ := h
    rw [mem_sieves_iff_hasEffectiveEpi]
    let x : (a : α) → (F.obj ⟨Z a⟩) := fun a ↦ (h' a).choose
    let _ : Fintype α := Fintype.ofFinite _
    let i' : ((a : α) → (F.obj ⟨Z a⟩)) ≅ (F.obj ⟨∐ Z⟩) :=
      (Types.productIso _).symm ≪≫ (PreservesProduct.iso F _).symm ≪≫ F.mapIso (opCoproductIsoProduct _).symm
    refine ⟨∐ Z, Sigma.desc π, inferInstance, i'.hom x, ?_⟩
    have := preservesLimitsOfShape_of_equiv (Discrete.opposite α).symm G
    apply Concrete.isLimit_ext _ (isLimitOfPreserves G (coproductIsCoproduct Z).op)
    intro ⟨⟨a⟩⟩
    simp only [Functor.comp_obj, Functor.op_obj, Discrete.functor_obj, Functor.mapCone_pt, Cocone.op_pt, Cofan.mk_pt,
      Functor.const_obj_obj, Functor.mapCone_π_app, Cocone.op_π, NatTrans.op_app, Cofan.mk_ι_app, Functor.mapIso_symm,
      Iso.symm_hom, Iso.trans_hom, Functor.mapIso_inv, types_comp_apply, i',
      ← NatTrans.naturality_apply f (Sigma.ι Z a).op]
    have : f.app ⟨Z a⟩ (x a) = G.map (π a).op y := (h' a).choose_spec
    convert this
    · change F.map _ (F.map _ _) = _
      rw [← FunctorToTypes.map_comp_apply, opCoproductIsoProduct_inv_comp_ι, ← piComparison_comp_π]
      change ((PreservesProduct.iso F _).hom ≫ _) _ = _
      have := Types.productIso_hom_comp_eval (fun a ↦ F.obj (op (Z a))) a
      rw [← Iso.eq_inv_comp] at this
      simp only [types_comp_apply, inv_hom_id_apply, congrFun this x]
    · change G.map _ (G.map _ _) = _
      simp only [← FunctorToTypes.map_comp_apply, ← op_comp, Sigma.ι_desc]

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