hornFilling — Mathlib

English

In a quasicategory S, every inner horn Λ[n,i] with 0 < i < last n admits a filler: for any σ0: Λ[n,i] → S there exists σ: Δ[n] → S with σ0 = Λ[n,i].ι σ.

Русский

В квази-категории S любой внутренний рог Λ[n,i] с 0 < i < last n допускает заполнение: для любого σ0: Λ[n,i] → S существует σ: Δ[n] → S, такой что σ0 = Λ[n,i].ι σ.

LaTeX

$$$\forall {S} [S.Quasicategory], \forall n, \forall i: Fin (n+1) \ (0

Lean4

theorem hornFilling {S : SSet} [Quasicategory S] ⦃n : ℕ⦄ ⦃i : Fin (n + 1)⦄ (h0 : 0 < i) (hn : i < Fin.last n)
    (σ₀ : (Λ[n, i] : SSet) ⟶ S) : ∃ σ : Δ[n] ⟶ S, σ₀ = Λ[n, i].ι ≫ σ := by
  cases n using Nat.casesAuxOn with
  | zero => simp [Fin.lt_iff_val_lt_val] at hn
  | succ n =>
    cases n using Nat.casesAuxOn with
    | zero =>
      simp only [Fin.lt_iff_val_lt_val, Fin.val_zero, Fin.val_last, zero_add, Nat.lt_one_iff] at h0 hn
      simp [hn] at h0
    | succ n => exact Quasicategory.hornFilling' σ₀ h0 hn

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