English
The 2-truncated nerve functor nerveFunctor₂ is full; every morphism between nerves arises from a morphism between the underlying simplicial structures.
Русский
2‑уровневый функтор нерва nerveFunctor₂ полон; каждый морфизм между нервами получается из морфизма между исходными симпликсами.
LaTeX
$$$\forall X,Y,\;\mathrm{Hom}(\mathrm{nerve}_2 X, \mathrm{nerve}_2 Y) \to \mathrm{Hom}(X,Y)$ is surjective$$
Lean4
instance full : nerveFunctor₂.{u, u}.Full where
map_surjective := by
intro X Y F
let uF := SSet.oneTruncation₂.map F
let uF' : X ⥤rq Y := OneTruncation₂.ofNerve₂.natIso.inv.app X ≫ uF ≫ OneTruncation₂.ofNerve₂.natIso.hom.app Y
have {a b c : X} (h : a ⟶ b) (k : b ⟶ c) : uF'.map (h ≫ k) = uF'.map h ≫ uF'.map k :=
by
let hk := ComposableArrows.mk₂ h k
let Fh : ComposableArrows Y 1 := F.app (op ⦋1⦌₂) (.mk₁ h)
let Fk : ComposableArrows Y 1 := F.app (op ⦋1⦌₂) (.mk₁ k)
let Fhk' : ComposableArrows Y 1 := F.app (op ⦋1⦌₂) (.mk₁ (h ≫ k))
let Fhk : ComposableArrows Y 2 := F.app (op ⦋2⦌₂) hk
have lem0 := congr_arg_heq (·.map' 0 1) (congr_fun (F.naturality δ0₂.op) hk)
have lem1 := congr_arg_heq (·.map' 0 1) (congr_fun (F.naturality δ1₂.op) hk)
have lem2 := congr_arg_heq (·.map' 0 1) (congr_fun (F.naturality δ2₂.op) hk)
have eq0 : (nerveFunctor₂.obj X).map δ0₂.op hk = .mk₁ k :=
by
apply ComposableArrows.ext₁ rfl rfl
simp [nerveFunctor₂, SSet.truncation]
have eq2 : (nerveFunctor₂.obj X).map δ2₂.op hk = .mk₁ h :=
by
apply ComposableArrows.ext₁ (by rfl) (by rfl)
simp [nerveFunctor₂, SSet.truncation]; rfl
have eq1 : (nerveFunctor₂.obj X).map δ1₂.op hk = .mk₁ (h ≫ k) :=
by
apply ComposableArrows.ext₁ (by rfl) (by rfl)
simp [nerveFunctor₂, SSet.truncation]; rfl
dsimp at lem0 lem1 lem2
rw [eq0] at lem0
rw [eq1] at lem1
rw [eq2] at lem2
replace lem0 : uF'.map k ≍ Fhk.map' 1 2 :=
by
refine HEq.trans (b := Fk.map' 0 1) ?_ lem0
simp [uF', nerveFunctor₂, SSet.truncation, ReflQuiv.comp_eq_comp, OneTruncation₂.nerveHomEquiv, Fk, uF]
replace lem2 : uF'.map h ≍ Fhk.map' 0 1 :=
by
refine HEq.trans (b := Fh.map' 0 1) ?_ lem2
simp [uF', nerveFunctor₂, SSet.truncation, ReflQuiv.comp_eq_comp, OneTruncation₂.nerveHomEquiv, uF,
ComposableArrows.hom, Fh]
replace lem1 : uF'.map (h ≫ k) ≍ Fhk.map' 0 2 :=
by
refine HEq.trans (b := Fhk'.map' 0 1) ?_ lem1
simp only [Nat.reduceAdd, Fin.zero_eta, Fin.isValue, Fin.mk_one, ComposableArrows.map', homOfLE_leOfHom, uF,
uF']
simp [nerveFunctor₂, SSet.truncation, ReflQuiv.comp_eq_comp, OneTruncation₂.nerveHomEquiv, ComposableArrows.hom,
Fhk']
rw [Fhk.map'_comp 0 1 2] at lem1
refine eq_of_heq (lem1.trans (heq_comp ?_ ?_ ?_ lem2.symm lem0.symm)) <;>
simp [uF', nerveFunctor₂, SSet.truncation, ReflQuiv.comp_eq_comp, uF, Fhk] <;>
[let ι := ι0₂; let ι := ι1₂; let ι := ι2₂] <;>
· replace := congr_arg (·.obj 0) (congr_fun (F.naturality ι.op) hk)
dsimp [oneTruncation₂, ComposableArrows.left, SimplicialObject.truncation, nerveFunctor₂, SSet.truncation,
forget₂, HasForget₂.forget₂] at this ⊢
convert this.symm
apply ComposableArrows.ext₀; rfl
let fF : X ⥤ Y := ReflPrefunctor.toFunctor uF' this
have eq : fF.toReflPrefunctor = uF' := rfl
refine ⟨fF, toNerve₂.ext (nerveFunctor₂.{u, u}.map fF) F ?_⟩
· have nat := OneTruncation₂.ofNerve₂.natIso.hom.naturality fF
simp at nat
rw [eq] at nat
simp [uF', uF] at nat
exact
(Iso.cancel_iso_hom_right (oneTruncation₂.map (nerveFunctor₂.map fF)) (oneTruncation₂.map F)
(OneTruncation₂.ofNerve₂.natIso.app Y)).mp
nat
