morphismProperty_eq_top — Mathlib

English

For multiplicative morphism properties on the truncated simplex category, the top element is forced by the defining δ, σ maps.

Русский

Для мультипликативного свойства морфизмов на усечённом простейлом категории верхний элемент определяется δ, σ-морфизмами.

LaTeX

$$$\\\\text{morphismProperty}_{Top} = \\\\text{top}$ in Truncated$$

Lean4

theorem 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; cutsat⟩ ⟶ ⟨.mk (n + 1), by dsimp; cutsat⟩))
    (σ_mem :
      ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)),
        W (SimplexCategory.σ (n := n) i : ⟨.mk (n + 1), by dsimp; cutsat⟩ ⟶ ⟨.mk n, by dsimp; cutsat⟩)) :
    W = ⊤ := by
  ext ⟨a, ha⟩ ⟨b, hb⟩ f
  simp only [MorphismProperty.top_apply, iff_true]
  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 cutsat
    obtain rfl : b = 0 := by cutsat
    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 cutsat)) (δ_mem _ (by cutsat) _)
    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 cutsat) _) (hc _ _ _ _ _ (by cutsat))
    rw [← epi_iff_surjective] at h₁
    rw [← mono_iff_injective] at h₂
    have := isIso_of_mono_of_epi f'
    obtain rfl : a = b := len_eq_of_isIso f'
    obtain rfl : f = 𝟙 _ := eq_id_of_mono f'
    apply W.id_mem

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