hasExt_iff_small_ext — Mathlib

English

HasExt is equivalent to Ext(X,Y,n) being small for all X,Y,n; equivalence with the smallness condition via small_congr Ext.homEquiv.

Русский

HasExt эквивалентен тому, что Ext(X,Y,n) является малым для всех X,Y,n; эквивалентность через small_congr Ext.homEquiv.

LaTeX

$$$HasExt \iff \forall X,Y,n, Small(Ext^n(X,Y))$$$

Lean4

theorem hasExt_iff_small_ext : HasExt.{w'} C ↔ ∀ (X Y : C) (n : ℕ), Small.{w'} (Ext.{w} X Y n) :=
  by
  letI := HasDerivedCategory.standard C
  simp only [hasExt_iff, small_congr Ext.homEquiv]
  constructor
  · intro h X Y n
    exact h X Y n (by simp)
  · intro h X Y n hn
    lift n to ℕ using hn
    exact h X Y n

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