[Merged by Bors] - feat(AlgebraicTopology): the simplex category (and its truncated versions) are generated by faces and degeneracies

[joelriou]

This allows to verify the naturality of morphisms between (truncated) (co)simplicial objects by checking only the naturality relative to the face and degeneracy maps.

Note: this is mostly independent of #21749 as the latter proves a stronger result, but only for SimplexCategory (not SimplexCategory.Truncated), which is already great enough!

---

[github-actions]

PR summary 9745c14a34

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (new file)	829

---

Declarations diff

+ Truncated.morphismProperty_eq_top
+ morphismProperty_eq_top
+ naturalityProperty
+ of_eq_top

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[emilyriehl]

The new code looks good. One organizational question: should SimplexCategory.lean now be moved to SimplexCategory/Basic.lean?

I've also been wondering whether it makes sense to break out the truncated stuff (not in your new code, but in the basic SimplexCategory file) into a separate file.

[emilyriehl]

I wonder if these lemmas would be more usable in the form that directly gives you that W f holds for any morphism f. Eg:

lemma Truncated.morphismProperty_from_δ_σ
    {d : ℕ} (W : MorphismProperty (Truncated d)) [W.IsMultiplicative]
    (δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)),
    W (SimplexCategory.δ (n := n) i : ⟨.mk n, by dsimp; omega⟩ ⟶
      ⟨.mk (n + 1), by dsimp; omega⟩))
    (σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)),
    W (SimplexCategory.σ (n := n) i : ⟨.mk (n + 1), by dsimp; omega⟩ ⟶
      ⟨.mk n, by dsimp; omega⟩))
    {a b : SimplexCategory} (ha : a.len ≤ d) (hb : b.len ≤ d)
    (f : ⟨a, ha⟩ ⟶ ⟨b, hb⟩) : W f := by
  induction' a using SimplexCategory.rec with a
  induction' b using SimplexCategory.rec with b
  dsimp at ha hb
  generalize h : a + b = c
  induction c generalizing a b with
  | zero =>
    obtain rfl : a = 0 := by omega
    obtain rfl : b = 0 := by omega
    obtain rfl : f = 𝟙 _ := by
      ext i : 3
      apply Subsingleton.elim (α := Fin 1)
    apply MorphismProperty.id_mem
  | succ c hc =>
    let f' : mk a ⟶ mk b := f
    by_cases h₁ : Function.Surjective f'.toOrderHom; swap
    · obtain _ | b := b
      · exact (h₁ (fun _ ↦ ⟨0, Subsingleton.elim (α := Fin 1) _ _⟩)).elim
      · obtain ⟨i, g', hf'⟩ := eq_comp_δ_of_not_surjective _ h₁
        obtain rfl : f = (g' : _ ⟶ ⟨mk b, by dsimp; omega⟩) ≫ δ i := hf'
        exact W.comp_mem _ _ (hc _ _ _ _ _ (by omega))
          (δ_mem _ (by omega) _)
    by_cases h₂ : Function.Injective f'.toOrderHom; swap
    · obtain _ | a := a
      · exact (h₂ (Function.injective_of_subsingleton (α := Fin 1) _)).elim
      · obtain ⟨i, g', hf'⟩ := eq_σ_comp_of_not_injective _ h₂
        obtain rfl : f = (by exact σ i) ≫ (g' : ⟨mk a, by dsimp; omega⟩ ⟶ _) := hf'
        exact W.comp_mem _ _ (σ_mem _ (by omega) _) (hc _ _ _ _ _ (by omega))
    rw [← epi_iff_surjective] at h₁
    rw [← mono_iff_injective] at h₂
    obtain rfl : a = b := le_antisymm (len_le_of_mono h₂) (len_le_of_epi h₁)
    obtain rfl : f = 𝟙 _ := eq_id_of_mono f'
    apply W.id_mem

lemma Truncated.morphismProperty_eq_top
    {d : ℕ} (W : MorphismProperty (Truncated d)) [W.IsMultiplicative]
    (δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)),
    W (SimplexCategory.δ (n := n) i : ⟨.mk n, by dsimp; omega⟩ ⟶
      ⟨.mk (n + 1), by dsimp; omega⟩))
    (σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)),
    W (SimplexCategory.σ (n := n) i : ⟨.mk (n + 1), by dsimp; omega⟩ ⟶
      ⟨.mk n, by dsimp; omega⟩)) :
    W = ⊤ := by
  ext ⟨a, ha⟩ ⟨b, hb⟩ f
  simp only [MorphismProperty.top_apply, iff_true]
  exact Truncated.morphismProperty_from_δ_σ W δ_mem σ_mem _ _ _

I'm thinking of the suggested application which is to show that naturality holds at an arbitrary morphism f.

[joelriou]

The new code looks good. One organizational question: should SimplexCategory.lean now be moved to SimplexCategory/Basic.lean?

Yes, I am anticipating on #21625.

I've also been wondering whether it makes sense to break out the truncated stuff (not in your new code, but in the basic SimplexCategory file) into a separate file.

In this case, I do not think it is important to do so.

Regarding the phrasing, I prefer statements of the form ... = ⊤, but to make this more usable in applications, it would be nice to add a version of https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/MorphismProperty/Basic.html#CategoryTheory.MorphismProperty.top_apply which would take an assumption of the form W = ⊤.

[emilyriehl]

I don't know how to suggest a change but here's the thing I think you're asking for which could go right after top_apply in MorphismProperty.Basic.lean:

lemma eq_top_apply (W : MorphismProperty C) (e : W = ⊤) {X Y : C} (f : X ⟶ Y) : W f := by
  rw [e]
  apply top_apply

[emilyriehl]

Looks great to me. Thanks for doing this.

[digama0]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build