From 231bfa3b0b9b3bf1a79066eb07654bf2144b3fb5 Mon Sep 17 00:00:00 2001 From: Nick Ward <102917377+gio256@users.noreply.github.com> Date: Fri, 7 Feb 2025 20:34:02 +0000 Subject: [PATCH] =?UTF-8?q?chore(AlgebraicTopology):=20autoParam=20for=20s?= =?UTF-8?q?trArrowMk=E2=82=82=20(#21562)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We make the proof in `SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂` an autoParam and remove the explicit proof term from most uses of `strArrowMk₂`. Additionally, we replace one instance of `erw` in the same file (`Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean`). --- .../SimplicialSet/Coskeletal.lean | 51 +++++++++---------- 1 file changed, 25 insertions(+), 26 deletions(-) diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean index 93eed2ed3a913..d5482f3a4008f 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean @@ -56,9 +56,9 @@ namespace isPointwiseRightKanExtensionAt /-- A morphism in `SimplexCategory` with domain `[0]`, `[1]`, or `[2]` defines an object in the comma category `StructuredArrow (op [n]) (Truncated.inclusion (n := 2)).op`.-/ -abbrev strArrowMk₂ {i : ℕ} {n : ℕ} (φ : [i] ⟶ [n]) (hi : i ≤ 2) : - StructuredArrow (op [n]) (Truncated.inclusion (n := 2)).op := - StructuredArrow.mk (Y := op ⟨[i], hi⟩) (by exact φ.op) +abbrev strArrowMk₂ {i : ℕ} {n : ℕ} (φ : [i] ⟶ [n]) (hi : i ≤ 2 := by omega) : + StructuredArrow (op [n]) (Truncated.inclusion 2).op := + StructuredArrow.mk (Y := op [i]₂) φ.op /-- Given a term in the cone over the diagram `(proj (op [n]) ((Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)` where `X` is @@ -71,15 +71,15 @@ noncomputable def lift {X : SSet.{u}} [StrictSegal X] {n} vertex := fun i ↦ s.π.app (.mk (Y := op [0]₂) (.op (SimplexCategory.const _ _ i))) x arrow := fun i ↦ s.π.app (.mk (Y := op [1]₂) (.op (mkOfLe _ _ (Fin.castSucc_le_succ i)))) x arrow_src := fun i ↦ by - let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) (by simp) ⟶ - strArrowMk₂ ([0].const _ i.castSucc) (by simp) := + let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶ + strArrowMk₂ ([0].const _ i.castSucc) := StructuredArrow.homMk (δ 1).op (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl)) exact congr_fun (s.w φ) x arrow_tgt := fun i ↦ by dsimp - let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) (by simp) ⟶ - strArrowMk₂ ([0].const _ i.succ) (by simp) := + let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶ + strArrowMk₂ ([0].const _ i.succ) := StructuredArrow.homMk (δ 0).op (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl)) exact congr_fun (s.w φ) x } @@ -88,7 +88,7 @@ lemma fac_aux₁ {n : ℕ} (s : Cone (proj (op [n]) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)) (x : s.pt) (i : ℕ) (hi : i < n) : X.map (mkOfSucc ⟨i, hi⟩).op (lift s x) = - s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩) (by omega)) x := by + s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩)) x := by dsimp [lift] rw [spineToSimplex_arrow] rfl @@ -97,18 +97,18 @@ lemma 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 omega⟩ ⟨j, by omega⟩ hij).op (lift s x) = - s.π.app (strArrowMk₂ (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ hij) (by omega)) x := by + s.π.app (strArrowMk₂ (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ 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 := by omega - have : mkOfLe ⟨i, Nat.lt_add_one_of_le hj⟩ ⟨i, Nat.lt_add_one_of_le hj⟩ (by omega) = + 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⟩) (by omega)) ⟶ - (strArrowMk₂ ([1].const [0] 0 ≫ [0].const [n] ⟨i, Nat.lt_add_one_of_le hj⟩) (by omega)) := + 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.Nat.cast_ofNat_Int, @@ -124,13 +124,12 @@ lemma fac_aux₂ {n : ℕ} | succ k hk => intro i j hij hj hik let α := strArrowMk₂ (mkOfLeComp (n := n) ⟨i, by omega⟩ ⟨i + k, by omega⟩ - ⟨j, by omega⟩ (by simp) - (by simp only [Fin.mk_le_mk]; omega)) (by rfl) + ⟨j, by omega⟩ (by simp) (by simp only [Fin.mk_le_mk]; omega)) let α₀ := strArrowMk₂ (mkOfLe (n := n) ⟨i + k, by omega⟩ ⟨j, by omega⟩ - (by simp only [Fin.mk_le_mk]; omega)) (by simp) + (by simp only [Fin.mk_le_mk]; omega)) let α₁ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨j, by omega⟩ - (by simp only [Fin.mk_le_mk]; omega)) (by simp) - let α₂ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨i + k, by omega⟩ (by simp)) (by simp) + (by simp only [Fin.mk_le_mk]; omega)) + let α₂ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨i + k, by omega⟩ (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 @@ -138,8 +137,8 @@ lemma fac_aux₂ {n : ℕ} let β₂ : α ⟶ α₂ := StructuredArrow.homMk ((mkOfSucc 0).op) (Quiver.Hom.unop_inj (by ext x; fin_cases x <;> rfl)) have h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x := by - obtain rfl : j = (i + k) + 1 := by omega - exact fac_aux₁ _ _ _ _ (by omega) + subst hik + exact fac_aux₁ _ _ _ _ hj have h₂ : X.map α₂.hom (lift s x) = s.π.app α₂ x := hk i (i + k) (by simp) (by omega) rfl change X.map α₁.hom (lift s x) = s.π.app α₁ x @@ -167,9 +166,9 @@ lemma fac_aux₂ {n : ℕ} lemma fac_aux₃ {n : ℕ} (s : Cone (proj (op [n]) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)) (x : s.pt) (φ : [1] ⟶ [n]) : - X.map φ.op (lift s x) = s.π.app (strArrowMk₂ φ (by omega)) x := by + X.map φ.op (lift s x) = s.π.app (strArrowMk₂ φ) x := by obtain ⟨i, j, hij, rfl⟩ : ∃ i j hij, φ = mkOfLe i j hij := - ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by simp), + ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by decide), Hom.ext_one_left _ _ rfl rfl⟩ exact fac_aux₂ _ _ _ _ _ _ (by omega) @@ -191,14 +190,14 @@ noncomputable def isPointwiseRightKanExtensionAt (n : ℕ) : dsimp ext k · dsimp only [spineEquiv, Equiv.coe_fn_mk] - erw [spine_map_vertex] - rw [spine_spineToSimplex, spine_vertex] - let α : strArrowMk₂ f hi ⟶ strArrowMk₂ ([0].const [n] (f.toOrderHom k)) (by omega) := + rw [show op f = f.op from rfl] + rw [spine_map_vertex, spine_spineToSimplex, spine_vertex] + let α : strArrowMk₂ f hi ⟶ strArrowMk₂ ([0].const [n] (f.toOrderHom k)) := StructuredArrow.homMk (([0].const _ (by exact k)).op) (by simp; rfl) exact congr_fun (s.w α).symm x · dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow] rw [← FunctorToTypes.map_comp_apply] - let α : strArrowMk₂ f hi ⟶ strArrowMk₂ (mkOfSucc k ≫ f) (by omega) := + let α : strArrowMk₂ f ⟶ strArrowMk₂ (mkOfSucc k ≫ f) := StructuredArrow.homMk (mkOfSucc k).op (by simp; rfl) exact (isPointwiseRightKanExtensionAt.fac_aux₃ _ _ _ _).trans (congr_fun (s.w α).symm x) uniq s m hm := by