Filtrations

In this file, a filtration on X indexed by a category I is defined as a functor I ⥤ MonoOver X.

We also define the category of filtered objects and strict morphisms, characterized by pullback squares at each filtration level.

Implementation notes

We model a filtration as a functor to MonoOver X, so that the filtration steps and their inclusions into X are bundled together and functorial in the index category.

References

• P. Deligne, Théorie de Hodge : II

structure CategoryTheory.Filtration {C : Type u} [Category.{v, u} C] (X : C) (I : Type u_1) [Category.{u_2, u_1} I] : Type (max (max (max u u_1) u_2) v)

A filtration on X indexed by I, as a functor I ⥤ MonoOver X.

• toMonoOver : Functor I (MonoOver X)

  The underlying functor I ⥤ MonoOver X.

@[reducible, inline]

abbrev CategoryTheory.Filtration.diagram {C : Type u} [Category.{v, u} C] {X : C} {I : Type u_1} [Category.{u_2, u_1} I] (F : Filtration X I) : Functor I C

The underlying diagram in C obtained by forgetting MonoOver.

Equations

• F.diagram = F.toMonoOver.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X))

theorem CategoryTheory.Filtration.diagram_obj {C : Type u} [Category.{v, u} C] {X : C} {I : Type u_1} [Category.{u_2, u_1} I] (F : Filtration X I) (X✝ : I) : F.diagram.obj X✝ = (F.toMonoOver.obj X✝).obj.left

theorem CategoryTheory.Filtration.diagram_map {C : Type u} [Category.{v, u} C] {X : C} {I : Type u_1} [Category.{u_2, u_1} I] (F : Filtration X I) {X✝ Y✝ : I} (f : X✝ ⟶ Y✝) : F.diagram.map f = Over.Hom.left (F.toMonoOver.map f).hom

@[reducible, inline]

abbrev CategoryTheory.Filtration.obj {C : Type u} [Category.{v, u} C] {X : C} {I : Type u_1} [Category.{u_2, u_1} I] (F : Filtration X I) (i : I) : C

The object at index i (domain of the mono into X).

Equations

• F.obj i = F.diagram.obj i

@[implicit_reducible]

def CategoryTheory.Filtration.ι {C : Type u} [Category.{v, u} C] {X : C} {I : Type u_1} [Category.{u_2, u_1} I] (F : Filtration X I) : F.diagram ⟶ (Functor.const I).obj X

The natural transformation from the filtration diagram to the constant underlying object.

Equations

• F.ι = { app := fun (i : I) => (F.toMonoOver.obj i).obj.hom, naturality := ⋯ }

theorem CategoryTheory.Filtration.ι_app {C : Type u} [Category.{v, u} C] {X : C} {I : Type u_1} [Category.{u_2, u_1} I] (F : Filtration X I) (i : I) : F.ι.app i = (F.toMonoOver.obj i).obj.hom

instance CategoryTheory.Filtration.instMonoAppι {C : Type u} [Category.{v, u} C] {X : C} {I : Type u_1} [Category.{u_2, u_1} I] (F : Filtration X I) (i : I) : Mono (F.ι.app i)

structure CategoryTheory.FilteredObject (C : Type u) [Category.{v, u} C] (I : Type u_1) [Category.{u_2, u_1} I] : Type (max (max (max u u_1) u_2) v)

A filtered object: an object equipped with a filtration.

• X : C

  The underlying object.

• filtration : Filtration self.X I

  The filtration on X.

@[reducible, inline]

abbrev CategoryTheory.FilteredObject.filtrationDiagram {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] (F : FilteredObject C I) : Functor I C

The filtration diagram in C.

Equations

• F.filtrationDiagram = F.filtration.diagram

structure CategoryTheory.FilteredObject.Hom {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] (F G : FilteredObject C I) : Type (max u_1 v)

Morphisms of filtered objects: a morphism on objects and a compatible natural transformation between the filtration diagrams.

• hom : F.X ⟶ G.X

  The underlying morphism on objects.

• natTrans : F.filtration.diagram ⟶ G.filtration.diagram

  The levelwise maps between filtration steps, natural in the index.

• comm (i : I) : CategoryStruct.comp (self.natTrans.app i) (G.filtration.ι.app i) = CategoryStruct.comp (F.filtration.ι.app i) self.hom

  Commutativity with the structure maps into the underlying objects.

theorem CategoryTheory.FilteredObject.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {I : Type u_1} {inst✝¹ : Category.{u_2, u_1} I} {F G : FilteredObject C I} {x y : F.Hom G} (hom : x.hom = y.hom) (natTrans : x.natTrans = y.natTrans) : x = y

theorem CategoryTheory.FilteredObject.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {I : Type u_1} {inst✝¹ : Category.{u_2, u_1} I} {F G : FilteredObject C I} {x y : F.Hom G} : x = y ↔ x.hom = y.hom ∧ x.natTrans = y.natTrans

@[simp]

theorem CategoryTheory.FilteredObject.Hom.comm_assoc {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} (self : F.Hom G) (i : I) {Z : C} (h : ((Functor.const I).obj G.X).obj i ⟶ Z) : CategoryStruct.comp (self.natTrans.app i) (CategoryStruct.comp (G.filtration.ι.app i) h) = CategoryStruct.comp (F.filtration.ι.app i) (CategoryStruct.comp self.hom h)

Commutativity with the structure maps into the underlying objects.

@[instance_reducible]

instance CategoryTheory.FilteredObject.instCategory {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] : Category.{max u_1 v, max (max (max u_2 u_1) u) v} (FilteredObject C I)

The category structure on filtered objects.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FilteredObject.id_hom {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] (x✝ : FilteredObject C I) : (CategoryStruct.id x✝).hom = CategoryStruct.id x✝.X

@[simp]

theorem CategoryTheory.FilteredObject.comp_hom {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {X✝ Y✝ Z✝ : FilteredObject C I} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

@[simp]

theorem CategoryTheory.FilteredObject.comp_natTrans {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {X✝ Y✝ Z✝ : FilteredObject C I} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).natTrans = CategoryStruct.comp f.natTrans g.natTrans

@[simp]

theorem CategoryTheory.FilteredObject.id_natTrans {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] (x✝ : FilteredObject C I) : (CategoryStruct.id x✝).natTrans = CategoryStruct.id x✝.filtration.diagram

theorem CategoryTheory.FilteredObject.hom_ext {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} {f g : F ⟶ G} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.FilteredObject.hom_ext_iff {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} {f g : F ⟶ G} : f = g ↔ f.hom = g.hom

@[implicit_reducible]

def CategoryTheory.FilteredObject.homMk {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} (hom : F.X ⟶ G.X) (app : (i : I) → F.filtration.obj i ⟶ G.filtration.obj i) (comm : ∀ (i : I), CategoryStruct.comp (app i) (G.filtration.ι.app i) = CategoryStruct.comp (F.filtration.ι.app i) hom := by cat_disch) : F ⟶ G

Constructor for morphisms of filtered objects.

Equations

• CategoryTheory.FilteredObject.homMk hom app comm = { hom := hom, natTrans := { app := app, naturality := ⋯ }, comm := comm }

@[simp]

theorem CategoryTheory.FilteredObject.homMk_hom {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} (hom : F.X ⟶ G.X) (app : (i : I) → F.filtration.obj i ⟶ G.filtration.obj i) (comm : ∀ (i : I), CategoryStruct.comp (app i) (G.filtration.ι.app i) = CategoryStruct.comp (F.filtration.ι.app i) hom := by cat_disch) : (homMk hom app comm).hom = hom

@[simp]

theorem CategoryTheory.FilteredObject.homMk_natTrans_app {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} (hom : F.X ⟶ G.X) (app : (i : I) → F.filtration.obj i ⟶ G.filtration.obj i) (comm : ∀ (i : I), CategoryStruct.comp (app i) (G.filtration.ι.app i) = CategoryStruct.comp (F.filtration.ι.app i) hom := by cat_disch) (i : I) : (homMk hom app comm).natTrans.app i = app i

@[implicit_reducible]

def CategoryTheory.FilteredObject.isoMk {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} (iso : F.X ≅ G.X) (app : (i : I) → F.filtration.obj i ≅ G.filtration.obj i) (comm : ∀ (i : I), CategoryStruct.comp (app i).hom (G.filtration.ι.app i) = CategoryStruct.comp (F.filtration.ι.app i) iso.hom := by cat_disch) : F ≅ G

Constructor for isomorphisms of filtered objects.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FilteredObject.isoMk_hom {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} (iso : F.X ≅ G.X) (app : (i : I) → F.filtration.obj i ≅ G.filtration.obj i) (comm : ∀ (i : I), CategoryStruct.comp (app i).hom (G.filtration.ι.app i) = CategoryStruct.comp (F.filtration.ι.app i) iso.hom := by cat_disch) : (isoMk iso app comm).hom = homMk iso.hom (fun (i : I) => (app i).hom) comm

@[simp]

theorem CategoryTheory.FilteredObject.isoMk_inv {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} (iso : F.X ≅ G.X) (app : (i : I) → F.filtration.obj i ≅ G.filtration.obj i) (comm : ∀ (i : I), CategoryStruct.comp (app i).hom (G.filtration.ι.app i) = CategoryStruct.comp (F.filtration.ι.app i) iso.hom := by cat_disch) : (isoMk iso app comm).inv = homMk iso.inv (fun (i : I) => (app i).inv) ⋯

class CategoryTheory.FilteredObject.IsStrictHom {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G : FilteredObject C I} (f : F ⟶ G) : Prop

Strictness of a filtered morphism: each compatibility square is a pullback.

• isPullback (i : I) : IsPullback (f.natTrans.app i) (F.filtration.ι.app i) (G.filtration.ι.app i) f.hom

  The square at each filtration step is a pullback square.

instance CategoryTheory.FilteredObject.instIsStrictHomId {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] (F : FilteredObject C I) : IsStrictHom (CategoryStruct.id F)

instance CategoryTheory.FilteredObject.instIsStrictHomComp {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {F G H : FilteredObject C I} (f : F ⟶ G) (g : G ⟶ H) [IsStrictHom f] [IsStrictHom g] : IsStrictHom (CategoryStruct.comp f g)

@[reducible, inline]

abbrev CategoryTheory.FilteredObject.isStrictHom (C : Type u) [Category.{v, u} C] (I : Type u_1) [Category.{u_2, u_1} I] : MorphismProperty (FilteredObject C I)

The morphism property of strict morphisms of filtered objects.

Equations

• CategoryTheory.FilteredObject.isStrictHom C I f = CategoryTheory.FilteredObject.IsStrictHom f

instance CategoryTheory.FilteredObject.instIsMultiplicativeIsStrictHom {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] : (isStrictHom C I).IsMultiplicative

@[implicit_reducible]

def CategoryTheory.FilteredObject.forget {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] : Functor (FilteredObject C I) C

The forgetful functor FilteredObject C I ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FilteredObject.forget_map {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] {X✝ Y✝ : FilteredObject C I} (f : X✝ ⟶ Y✝) : forget.map f = f.hom

@[simp]

theorem CategoryTheory.FilteredObject.forget_obj {C : Type u} [Category.{v, u} C] {I : Type u_1} [Category.{u_2, u_1} I] (A : FilteredObject C I) : forget.obj A = A.X