English
A second auxiliary lemma for the pointwise right Kan extension; establishes a coherence between lift along a morphism and a cone map on a higher simplex.
Русский
Вторая вспомогательная лемма для точного правого кан-расширения; устанавливает когерентность между подъемом по морфизму и конусной картой на большем симпликсе.
LaTeX
$$$ \\text{fac\_aux}_2 \\]$$$
Lean4
theorem fac_aux₂ {n : ℕ} (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
(x : s.pt) (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n) :
X.map (mkOfLe ⟨i, by cutsat⟩ ⟨j, by cutsat⟩ hij).op (lift sx s x) =
s.π.app (strArrowMk₂ (mkOfLe ⟨i, by cutsat⟩ ⟨j, by cutsat⟩ hij)) x :=
by
obtain ⟨k, hk⟩ := Nat.le.dest hij
revert i j
induction k with
| zero =>
rintro i j hij hj hik
obtain rfl : i = j := hik
have :
mkOfLe ⟨i, Nat.lt_add_one_of_le hj⟩ ⟨i, Nat.lt_add_one_of_le hj⟩ (by rfl) =
⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩ :=
Hom.ext_one_left _ _
rw [this]
let α :
(strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩)) ⟶
(strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, Nat.lt_add_one_of_le hj⟩)) :=
StructuredArrow.homMk ((⦋1⦌.const ⦋0⦌ 0).op) (by simp; rfl)
have nat := congr_fun (s.π.naturality α) x
dsimp only [Fin.val_zero, Nat.add_zero, id_eq, Int.reduceNeg, Int.cast_ofNat_Int, Int.reduceAdd, Fin.eta, comp_obj,
StructuredArrow.proj_obj, op_obj, const_obj_obj, const_obj_map, types_comp_apply, types_id_apply,
Functor.comp_map, StructuredArrow.proj_map, op_map] at nat
rw [nat, op_comp, Functor.map_comp]
simp only [types_comp_apply]
refine congrArg (X.map (⦋1⦌.const ⦋0⦌ 0).op) ?_
unfold strArrowMk₂
rw [lift, StrictSegal.spineToSimplex_vertex]
congr
| succ k hk =>
intro i j hij hj hik
let α :=
strArrowMk₂
(mkOfLeComp (n := n) ⟨i, by cutsat⟩ ⟨i + k, by cutsat⟩ ⟨j, by cutsat⟩ (by simp)
(by simp only [Fin.mk_le_mk]; cutsat))
let α₀ := strArrowMk₂ (mkOfLe (n := n) ⟨i + k, by cutsat⟩ ⟨j, by cutsat⟩ (by simp only [Fin.mk_le_mk]; cutsat))
let α₁ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by cutsat⟩ ⟨j, by cutsat⟩ hij)
let α₂ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by cutsat⟩ ⟨i + k, by cutsat⟩ (by simp))
let β₀ : α ⟶ α₀ := StructuredArrow.homMk ((mkOfSucc 1).op) (Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl))
let β₁ : α ⟶ α₁ := StructuredArrow.homMk ((δ 1).op) (Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl))
let β₂ : α ⟶ α₂ := StructuredArrow.homMk ((mkOfSucc 0).op) (Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl))
have h₀ : X.map α₀.hom (lift sx s x) = s.π.app α₀ x :=
by
subst hik
exact fac_aux₁ _ _ _ _ hj
have h₂ : X.map α₂.hom (lift sx s x) = s.π.app α₂ x := hk i (i + k) (by simp) (by cutsat) rfl
change X.map α₁.hom (lift sx s x) = s.π.app α₁ x
have : X.map α.hom (lift sx s x) = s.π.app α x :=
by
apply sx.spineInjective
apply Path.ext'
intro t
dsimp only [spineEquiv]
rw [Equiv.coe_fn_mk, spine_arrow, spine_arrow, ← FunctorToTypes.map_comp_apply]
match t with
| 0 =>
have : α.hom ≫ (mkOfSucc 0).op = α₂.hom := Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl)
rw [this, h₂, ← congr_fun (s.w β₂) x]
rfl
| 1 =>
have : α.hom ≫ (mkOfSucc 1).op = α₀.hom := Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl)
rw [this, h₀, ← congr_fun (s.w β₀) x]
rfl
rw [← StructuredArrow.w β₁, FunctorToTypes.map_comp_apply, this, ← s.w β₁]
dsimp
