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_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Precoherent C] (e : C ≌ D) :

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.instIsDenseSubsiteCoherentTopologyInverse {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Precoherent C] (e : C ≌ D) :

CategoryTheory.Functor.IsDenseSubsite (CategoryTheory.coherentTopology D) (CategoryTheory.coherentTopology C) e.inverse

Equations

⋯ = ⋯

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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) :

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

Equivalent precoherent categories give equivalent coherent toposes.

Equations

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

Instances For

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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X : Dᵒᵖ) :

((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).functor.obj F).val.obj X = F.val.obj (Opposite.op (e.inverse.obj (Opposite.unop X)))

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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) (X : Dᵒᵖ) :

((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).counitIso.hom.app X✝).val.app X = X✝.val.map (e.counitIso.inv.app (Opposite.unop X)).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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) :

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

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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X : Cᵒᵖ) :

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

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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) :

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

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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) :

∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).inverse.obj F).val.map f = F.val.map (e.functor.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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) (X : Dᵒᵖ) :

((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).counitIso.inv.app X✝).val.app X = X✝.val.map (e.counitIso.hom.app (Opposite.unop X)).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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) :

∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).functor.obj F).val.map f = F.val.map (e.inverse.map f.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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) (X : Cᵒᵖ) :

((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).inverse.obj F).val.obj X = F.val.obj (Opposite.op (e.functor.obj (Opposite.unop X)))

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] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X : Cᵒᵖ) :

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

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_5, u_2} D] [CategoryTheory.Precoherent C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (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_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preregular C] (e : C ≌ D) :

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.instIsDenseSubsiteRegularTopologyInverse {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preregular C] (e : C ≌ D) :

CategoryTheory.Functor.IsDenseSubsite (CategoryTheory.regularTopology D) (CategoryTheory.regularTopology C) e.inverse

Equations

⋯ = ⋯

source

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

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

Equivalent preregular categories give equivalent regular toposes.

Equations

CategoryTheory.Equivalence.sheafCongrPreregular A e = CategoryTheory.Equivalence.sheafCongr (CategoryTheory.regularTopology C) (CategoryTheory.regularTopology D) e A

Instances For

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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) (X : Dᵒᵖ) :

((CategoryTheory.Equivalence.sheafCongrPreregular A e).counitIso.hom.app X✝).val.app X = X✝.val.map (e.counitIso.inv.app (Opposite.unop X)).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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) :

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

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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) :

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

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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (F : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) :

∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongrPreregular A e).inverse.obj F).val.map f = F.val.map (e.functor.map f.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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (F : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) :

∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongrPreregular A e).functor.obj F).val.map f = F.val.map (e.inverse.map f.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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) (X : Cᵒᵖ) :

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

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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (F : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) (X : Dᵒᵖ) :

((CategoryTheory.Equivalence.sheafCongrPreregular A e).functor.obj F).val.obj X = F.val.obj (Opposite.op (e.inverse.obj (Opposite.unop X)))

source

@[simp]

theorem CategoryTheory.Equivalence.sheafCongrPreregular_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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) (X : Dᵒᵖ) :

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

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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (F : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) (X : Cᵒᵖ) :

((CategoryTheory.Equivalence.sheafCongrPreregular A e).inverse.obj F).val.obj X = F.val.obj (Opposite.op (e.functor.obj (Opposite.unop X)))

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] [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] (e : C ≌ D) (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) (X : Cᵒᵖ) :

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

source

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

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

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

source

theorem CategoryTheory.Equivalence.preregular_isSheaf_iff_of_essentiallySmall {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preregular 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.regularTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology (CategoryTheory.SmallModel.{u_4, u_5, u_1} C)) ((CategoryTheory.equivSmallModel C).inverse.op.comp F)

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

Documentation

Mathlib.CategoryTheory.Sites.Coherent.Equivalence

Coherence and equivalence of categories #