Documentation

Atlas.TensorCategories.code.Ext1UnitVanishing

source
def TensorCategories.Ext1Vanishes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X Y : C) :
Prop

The predicate Ext¹(X, Y) = 0 expressed as: every short exact sequence 0 → Y → V → X → 0 splits.

Instances For
    source
    theorem TensorCategories.Ext1Vanishes.exists_section {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (h : Ext1Vanishes X Y) {V : C} {f : Y ⟶ V} {g : V ⟶ X} {hfg : CategoryTheory.CategoryStruct.comp f g = 0} (hse : { X₁ := Y, X₂ := V, X₃ := X, f := f, g := g, zero := hfg }.ShortExact) :
    ∃ (s : X ⟶ V), CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id X

    If Ext¹(X, Y) = 0, then any short exact sequence 0 → Y → V → X → 0 admits a section s : X ⟶ V of g.

    source
    theorem TensorCategories.Ext1Vanishes.exists_retraction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (h : Ext1Vanishes X Y) {V : C} {f : Y ⟶ V} {g : V ⟶ X} {hfg : CategoryTheory.CategoryStruct.comp f g = 0} (hse : { X₁ := Y, X₂ := V, X₃ := X, f := f, g := g, zero := hfg }.ShortExact) :
    ∃ (r : V ⟶ Y), CategoryTheory.CategoryStruct.comp f r = CategoryTheory.CategoryStruct.id Y

    If Ext¹(X, Y) = 0, then any short exact sequence 0 → Y → V → X → 0 admits a retraction r : V ⟶ Y of f.

    source
    theorem TensorCategories.Ext1Vanishes.full_splitting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (h : Ext1Vanishes X Y) {V : C} {f : Y ⟶ V} {g : V ⟶ X} {hfg : CategoryTheory.CategoryStruct.comp f g = 0} (hse : { X₁ := Y, X₂ := V, X₃ := X, f := f, g := g, zero := hfg }.ShortExact) :
    ∃ (r : V ⟶ Y) (s : X ⟶ V), CategoryTheory.CategoryStruct.comp f r = CategoryTheory.CategoryStruct.id Y ∧ CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp r f + CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id V

    If Ext¹(X, Y) = 0, then any short exact sequence 0 → Y → V → X → 0 admits both a retraction r of f and a section s of g satisfying the bi-product identity.

    source
    theorem TensorCategories.Ext1Vanishes.splitting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (h : Ext1Vanishes X Y) {S : CategoryTheory.ShortComplex C} (hse : S.ShortExact) (hX : S.X₃ = X) (hY : S.X₁ = Y) :
    Nonempty S.Splitting

    Version of the splitting consequence of Ext1Vanishes phrased for an arbitrary short complex whose endpoints match X and Y.

    source
    class TensorCategories.FiniteRingCategory (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.MonoidalCategory C, CategoryTheory.Abelian C, CategoryTheory.Linear k C :
    Type (max (max u v) w)

    A k-linear abelian monoidal category that has enough projectives and finite- dimensional Hom spaces; this is the underlying ring-category structure used in EGNO.

    Instances
      source
      theorem TensorCategories.FiniteRingCategory.enough_projectives (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [FiniteRingCategory k C] :
      CategoryTheory.EnoughProjectives C

      A FiniteRingCategory has enough projectives.

      source
      theorem TensorCategories.FiniteRingCategory.hom_finite_dimensional (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [FiniteRingCategory k C] (X Y : C) :
      FiniteDimensional k (X ⟶ Y)

      Hom spaces in a FiniteRingCategory are finite-dimensional over the base field.

      source
      @[implicit_reducible, instance 100]
      instance TensorCategories.FiniteRingCategory.ofFiniteTensorCategory (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.FiniteTensorCategory k C] :
      FiniteRingCategory k C

      Every finite tensor category over k carries the underlying structure of a FiniteRingCategory over k.

      source
      class TensorCategories.HasDerivationFromExtension (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [FiniteRingCategory k C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] :
      Prop

      Existence hypothesis: from a non-split extension of 𝟙_ C by 𝟙_ C one can build a higher derivation system on some finite-dimensional k-algebra with nonzero first coefficient χ 1.

      Instances
        source
        theorem TensorCategories.derivation_from_nonsplit_ext (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [FiniteRingCategory k C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] (V : C) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ V) (g : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (hfg : CategoryTheory.CategoryStruct.comp f g = 0) (hse : { X₁ := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, X₂ := V, X₃ := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, f := f, g := g, zero := hfg }.ShortExact) (hns : ¬Nonempty { X₁ := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, X₂ := V, X₃ := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, f := f, g := g, zero := hfg }.Splitting) :
        ∃ (A : Type w) (x : Ring A) (x_1 : Algebra k A) (_ : FiniteDimensional k A) (ε : A →ₐ[k] k) (hds : HigherDerivationSystem k A ε), hds.χ 1 ≠ 0

        From a non-split extension of 𝟙_ C by 𝟙_ C one obtains a higher derivation system on some finite-dimensional k-algebra whose first coefficient is nonzero.

        source
        instance TensorCategories.instHasDerivationFromExtension (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [FiniteRingCategory k C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] :
        HasDerivationFromExtension k C

        The class HasDerivationFromExtension is automatically satisfied in any finite ring category with a simple unit, via derivation_from_nonsplit_ext.

        source
        theorem TensorCategories.ext1Vanishes_unit_unit_of_charZero (k : Type w) [Field k] [CharZero k] (C : Type u) [CategoryTheory.Category.{v, u} C] [FiniteRingCategory k C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] [HasDerivationFromExtension k C] [HasHigherDerivationContradiction k] :
        Ext1Vanishes (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

        In characteristic zero, Ext¹(𝟙_ C, 𝟙_ C) vanishes in any finite ring category with simple unit, by contradiction with the higher derivation construction.