Coherence and equivalence of categories #

This file proves that the coherent and regular topologies transfer nicely along equivalences of categories.

theorem CategoryTheory.Equivalence.precoherent {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] :

CategoryTheory.Precoherent D

Precoherent is preserved by equivalence of categories.

source

instance CategoryTheory.Equivalence.instPrecoherentSmallModel {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Precoherent C] [CategoryTheory.EssentiallySmall.{u_3, u_4, u_1} C] :

CategoryTheory.Precoherent (CategoryTheory.SmallModel.{u_3, u_4, u_1} C)

Equations

⋯ = ⋯

source

instance CategoryTheory.Equivalence.instTransportsGrothendieckTopologyCoherentTopology {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] :

CategoryTheory.Equivalence.TransportsGrothendieckTopology (CategoryTheory.coherentTopology C) (CategoryTheory.coherentTopology D) e

Equations

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X : Cᵒᵖ) :

((e.sheafCongrPrecoherent A).unitIso.hom.app X✝).val.app X = X✝.val.map (e.unitIso.inv.app X.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X : Cᵒᵖ) :

((e.sheafCongrPrecoherent A).unitIso.inv.app X✝).val.app X = X✝.val.map (e.unitIso.hom.app X.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_val_map {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) :

∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((e.sheafCongrPrecoherent A).inverse.obj F).val.map f = F.val.map (e.functor.map f.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_val_map {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) :

∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((e.sheafCongrPrecoherent A).functor.obj F).val.map f = F.val.map (e.inverse.map f.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) (X : Dᵒᵖ) :

((e.sheafCongrPrecoherent A).counitIso.inv.app X✝).val.app X = X✝.val.map (e.counitIso.hom.app X.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_val_obj {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) (X : Cᵒᵖ) :

((e.sheafCongrPrecoherent A).inverse.obj F).val.obj X = F.val.obj { unop := e.functor.obj X.unop }

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] :

∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A} (f : X ⟶ Y) (X_1 : Cᵒᵖ), ((e.sheafCongrPrecoherent A).inverse.map f).val.app X_1 = f.val.app { unop := e.functor.obj X_1.unop }

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) (X : Dᵒᵖ) :

((e.sheafCongrPrecoherent A).counitIso.hom.app X✝).val.app X = X✝.val.map (e.counitIso.inv.app X.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] :

∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A} (f : X ⟶ Y) (X_1 : Dᵒᵖ), ((e.sheafCongrPrecoherent A).functor.map f).val.app X_1 = f.val.app { unop := e.inverse.obj X_1.unop }

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_val_obj {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X : Dᵒᵖ) :

((e.sheafCongrPrecoherent A).functor.obj F).val.obj X = F.val.obj { unop := e.inverse.obj X.unop }

source

def CategoryTheory.Equivalence.sheafCongrPrecoherent {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] :

CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A ≌ CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A

Equivalent precoherent categories give equivalent coherent toposes.

Equations

e.sheafCongrPrecoherent A = CategoryTheory.Equivalence.sheafCongr (CategoryTheory.coherentTopology C) (CategoryTheory.coherentTopology D) e A

Instances For

source

theorem CategoryTheory.Equivalence.precoherent_isSheaf_iff {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_6, u_2} D] (e : C ≌ D) [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_5, u_3} A] (F : CategoryTheory.Functor Cᵒᵖ A) :

CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology D) (e.inverse.op.comp F)

The coherent sheaf condition can be checked after precomposing with the equivalence.

source

theorem CategoryTheory.Equivalence.precoherent_isSheaf_iff_of_essentiallySmall {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.EssentiallySmall.{u_4, u_5, u_1} C] (F : CategoryTheory.Functor Cᵒᵖ A) :

CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology (CategoryTheory.SmallModel.{u_4, u_5, u_1} C)) ((CategoryTheory.equivSmallModel C).inverse.op.comp F)

The coherent sheaf condition on an essentially small site can be checked after precomposing with the equivalence with a small category.

source

theorem CategoryTheory.Equivalence.preregular {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] :

CategoryTheory.Preregular D

Preregular is preserved by equivalence of categories.

source

instance CategoryTheory.Equivalence.instPreregularSmallModel {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preregular C] [CategoryTheory.EssentiallySmall.{u_3, u_4, u_1} C] :

CategoryTheory.Preregular (CategoryTheory.SmallModel.{u_3, u_4, u_1} C)

Equations

⋯ = ⋯

source

instance CategoryTheory.Equivalence.instTransportsGrothendieckTopologyRegularTopology {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] :

CategoryTheory.Equivalence.TransportsGrothendieckTopology (CategoryTheory.regularTopology C) (CategoryTheory.regularTopology D) e

Equations

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_val_obj {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) (X : Cᵒᵖ) :

((e.sheafCongrPreregular A).inverse.obj F).val.obj X = F.val.obj { unop := e.functor.obj X.unop }

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_val_obj {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) (X : Dᵒᵖ) :

((e.sheafCongrPreregular A).functor.obj F).val.obj X = F.val.obj { unop := e.inverse.obj X.unop }

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_val_map {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) :

∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((e.sheafCongrPreregular A).inverse.obj F).val.map f = F.val.map (e.functor.map f.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) (X : Dᵒᵖ) :

((e.sheafCongrPreregular A).counitIso.hom.app X✝).val.app X = X✝.val.map (e.counitIso.inv.app X.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) (X : Cᵒᵖ) :

((e.sheafCongrPreregular A).unitIso.hom.app X✝).val.app X = X✝.val.map (e.unitIso.inv.app X.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_val_map {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (F : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) :

∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((e.sheafCongrPreregular A).functor.obj F).val.map f = F.val.map (e.inverse.map f.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_functor_map_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] :

∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A} (f : X ⟶ Y) (X_1 : Dᵒᵖ), ((e.sheafCongrPreregular A).functor.map f).val.app X_1 = f.val.app { unop := e.inverse.obj X_1.unop }

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) (X : Cᵒᵖ) :

((e.sheafCongrPreregular A).unitIso.inv.app X✝).val.app X = X✝.val.map (e.unitIso.hom.app X.unop).op

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_inverse_map_val_app {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] :

∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A} (f : X ⟶ Y) (X_1 : Cᵒᵖ), ((e.sheafCongrPreregular A).inverse.map f).val.app X_1 = f.val.app { unop := e.functor.obj X_1.unop }

source

@[simp]