Enhanced derived categories of sheaves

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

InstanceThe lax monoidal structure of the Dold–Kan functor Γ from chain complexes to simplicial objects#

it is the mate, along the Dold–Kan equivalence, of the Alexander–Whitney oplax monoidal structure of the normalized chain functor N (CategoryTheory.Idempotents.DoldKan.Γ_ε and CategoryTheory.Idempotents.DoldKan.Γ_μ).

CategoryTheory.Idempotents.DoldKan.laxMonoidalΓ.{v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] :
  CategoryTheory.Idempotents.DoldKan.Γ.LaxMonoidal
Lean

Formalized in Tau Ceti as CategoryTheory.Idempotents.DoldKan.laxMonoidalΓ.

Sources
LeanCategoryTheory.Idempotents.DoldKan.laxMonoidalΓ
Uses 1
Proof usesCoassociativity of the Alexander–Whitney map

TheoremCoassociativity of the Alexander–Whitney map#

the two ways of splitting a simplex into a front, a middle and a back face agree, up to the associators of simplicial objects and of chain complexes.

CategoryTheory.SimplicialObject.alexanderWhitney_coassoc.{v, u} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C]
  [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [CategoryTheory.Limits.HasFiniteCoproducts C] (A B D : CategoryTheory.SimplicialObject C) :
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj A B).alexanderWhitney D)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (A.alexanderWhitney B)
          ((AlgebraicTopology.alternatingFaceMapComplex C).obj D))
        (CategoryTheory.MonoidalCategoryStruct.associator
            ((AlgebraicTopology.alternatingFaceMapComplex C).obj A)
            ((AlgebraicTopology.alternatingFaceMapComplex C).obj B)
            ((AlgebraicTopology.alternatingFaceMapComplex C).obj D)).hom) =
    CategoryTheory.CategoryStruct.comp
      ((AlgebraicTopology.alternatingFaceMapComplex C).map
        (CategoryTheory.MonoidalCategoryStruct.associator A B D).hom)
      (CategoryTheory.CategoryStruct.comp
        (A.alexanderWhitney (CategoryTheory.MonoidalCategoryStruct.tensorObj B D))
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          ((AlgebraicTopology.alternatingFaceMapComplex C).obj A) (B.alexanderWhitney D)))
Lean

Formalized in Tau Ceti as CategoryTheory.SimplicialObject.alexanderWhitney_coassoc.

Sources
LeanCategoryTheory.SimplicialObject.alexanderWhitney_coassoc
Used by 1
Used byThe lax monoidal structure of the Dold–Kan functor Γ from chain complexes to simplicial objects

TheoremFrobenius-root ideals are radicals#

In a perfect ring, the Frobenius-root ideal of f is the radical of the principal ideal (f).

TauCeti.frobeniusRootIdeal_eq_radical.{u_1} {R : Type u_1} [CommSemiring R] {p : ℕ} [ExpChar R p]
  [PerfectRing R p] [hp : Fact (Nat.Prime p)] (f : R) :
  TauCeti.frobeniusRootIdeal R p f = (Ideal.span {f}).radical
Lean

Formalized in Tau Ceti as TauCeti.frobeniusRootIdeal_eq_radical.

Sources
LeanTauCeti.frobeniusRootIdeal_eq_radical

TheoremFrobenius-root ideals are flat, also when R has zero divisors# 

TauCeti.flat_frobeniusRootIdeal.{u_1} {R : Type u_1} [CommRing R] {p : ℕ} [ExpChar R p]
  [PerfectRing R p] [hp : Fact (Nat.Prime p)] (f : R) :
  Module.Flat R ↥(TauCeti.frobeniusRootIdeal R p f)
Lean

Formalized in Tau Ceti as TauCeti.flat_frobeniusRootIdeal.

Sources
LeanTauCeti.flat_frobeniusRootIdeal

TheoremThe multiplication tower is pro-zero exactly for nilpotent elements# 

TauCeti.ModuleTower.isProZero_multiplicationTower_iff.{u} {R : Type u} [Ring R] (a : R) :
  CategoryTheory.Functor.IsProZero (TauCeti.ModuleTower.multiplicationTower a) ↔ IsNilpotent a
Lean

Formalized in Tau Ceti as TauCeti.ModuleTower.isProZero_multiplicationTower_iff.

Sources
LeanTauCeti.ModuleTower.isProZero_multiplicationTower_iff
Uses 1
Statement usesCategoryTheory.Functor.IsProZero

DefinitionCategoryTheory.Functor.IsProZero#

A diagram F : J ⥤ C is pro-zero if every object F j is killed by some map of the diagram: for every j there is f : i ⟶ j with F.map f = 0. For towers ℕᵒᵖ ⥤ C this says that every term is killed by some later composite transition (isProZero_iff_forall_exists_le).

CategoryTheory.Functor.IsProZero.{v₁, v₂, u₁, u₂} {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J]
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J C) : Prop
Lean

Formalized in Tau Ceti as CategoryTheory.Functor.IsProZero.

Sources
LeanCategoryTheory.Functor.IsProZero
Used by 2
Used byCategoryTheory.Functor.proIsomorphisms · The multiplication tower is pro-zero exactly for nilpotent elements

AbbreviationCategoryTheory.Functor.proIsomorphisms#

The pro-isomorphisms of diagrams J ⥤ C: the morphisms whose kernel and cokernel are pro-zero (proIsomorphisms_iff). This is Mathlib's class ObjectProperty.isoModSerre of isomorphisms modulo the Serre class of pro-zero diagrams, so pro-isomorphisms are stable under composition and retracts and satisfy two-out-of-three.

CategoryTheory.Functor.proIsomorphisms.{v₁, v₂, u₁, u₂} (J : Type u₁)
  [CategoryTheory.Category.{v₁, u₁} J] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C]
  [CategoryTheory.Abelian C] : CategoryTheory.MorphismProperty (CategoryTheory.Functor J C)
Lean

Formalized in Tau Ceti as CategoryTheory.Functor.proIsomorphisms.

Sources
LeanCategoryTheory.Functor.proIsomorphisms
Uses 1
Statement usesCategoryTheory.Functor.IsProZero

DefinitionSSet.fullEnhancedSubcategory#

The full enhanced subcategory of a simplicial set X on a predicate P on its vertices: the subcomplex of the simplices all of whose vertices satisfy P.

SSet.fullEnhancedSubcategory.{u} (X : _root_.SSet) (P : X.obj (Opposite.op { len := 0 }) → Prop) :
  X.Subcomplex
Lean

Formalized in Tau Ceti as SSet.fullEnhancedSubcategory.

Sources
LeanSSet.fullEnhancedSubcategory

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.