Documentation

Mathlib.CategoryTheory.Sites.Coherent.Equivalence

Coherence and equivalence of categories #

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

source
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.instPrecoherentSmallModelSmallCategorySmallModel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Precoherent C] [CategoryTheory.EssentiallySmall.{u_4, u_3, u_1} C] :
CategoryTheory.Precoherent (CategoryTheory.SmallModel.{u_4, u_3, u_1} C)
Equations
  • ⋯ = ⋯
source
theorem CategoryTheory.Equivalence.precoherent_eq {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.LocallyCoverDense.inducedTopology ⋯ = CategoryTheory.coherentTopology D

Transferring the coherent topology along an equivalence of categories gives the coherent topology.

source
instance CategoryTheory.Equivalence.instTransportsGrothendieckTopologyCoherentTopologyCoherentTopologyPrecoherent {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_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ᵒᵖ) :
((CategoryTheory.Equivalence.sheafCongrPrecoherent e A).functor.obj F).val.obj X = F.val.obj (Opposite.op (e.inverse.obj X.unop))
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ᵒᵖ) :
((CategoryTheory.Equivalence.sheafCongrPrecoherent e A).unitIso.hom.app X✝).val.app X = X✝.val.map (e.unitIso.inv.app X.unop).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] (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ᵒᵖ), ((CategoryTheory.Equivalence.sheafCongrPrecoherent e A).inverse.map f).val.app X_1 = f.val.app (Opposite.op (e.functor.obj X_1.unop))
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ᵒᵖ) :
((CategoryTheory.Equivalence.sheafCongrPrecoherent e 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), ((CategoryTheory.Equivalence.sheafCongrPrecoherent e 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), ((CategoryTheory.Equivalence.sheafCongrPrecoherent e 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ᵒᵖ) :
((CategoryTheory.Equivalence.sheafCongrPrecoherent e A).counitIso.inv.app X✝).val.app X = X✝.val.map (e.counitIso.hom.app X.unop).op
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ᵒᵖ) :
((CategoryTheory.Equivalence.sheafCongrPrecoherent e 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ᵒᵖ), ((CategoryTheory.Equivalence.sheafCongrPrecoherent e A).functor.map f).val.app X_1 = f.val.app (Opposite.op (e.inverse.obj X_1.unop))
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ᵒᵖ) :
((CategoryTheory.Equivalence.sheafCongrPrecoherent e A).inverse.obj F).val.obj X = F.val.obj (Opposite.op (e.functor.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
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) (CategoryTheory.Functor.comp e.inverse.op 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.Functor.comp (CategoryTheory.equivSmallModel C).inverse.op 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.instPreregularSmallModelSmallCategorySmallModel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preregular C] [CategoryTheory.EssentiallySmall.{u_4, u_3, u_1} C] :
    CategoryTheory.Preregular (CategoryTheory.SmallModel.{u_4, u_3, u_1} C)
    Equations
    • ⋯ = ⋯
    source
    theorem CategoryTheory.Equivalence.preregular_eq {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.LocallyCoverDense.inducedTopology ⋯ = CategoryTheory.regularTopology D

    Transferring the regular topology along an equivalence of categories gives the regular topology.

    source
    instance CategoryTheory.Equivalence.instTransportsGrothendieckTopologyRegularTopologyRegularTopologyPreregular {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ᵒᵖ) :
    ((CategoryTheory.Equivalence.sheafCongrPreregular e A).inverse.obj F).val.obj X = F.val.obj (Opposite.op (e.functor.obj X.unop))
    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] (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ᵒᵖ) :
    ((CategoryTheory.Equivalence.sheafCongrPreregular e A).counitIso.inv.app X✝).val.app X = X✝.val.map (e.counitIso.hom.app X.unop).op
    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ᵒᵖ) :
    ((CategoryTheory.Equivalence.sheafCongrPreregular e A).unitIso.inv.app X✝).val.app X = X✝.val.map (e.unitIso.hom.app X.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ᵒᵖ) :
    ((CategoryTheory.Equivalence.sheafCongrPreregular e A).counitIso.hom.app X✝).val.app X = X✝.val.map (e.counitIso.inv.app X.unop).op
    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), ((CategoryTheory.Equivalence.sheafCongrPreregular e A).inverse.obj F).val.map f = F.val.map (e.functor.map f.unop).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] (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ᵒᵖ) :
    ((CategoryTheory.Equivalence.sheafCongrPreregular e A).functor.obj F).val.obj X = F.val.obj (Opposite.op (e.inverse.obj X.unop))
    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ᵒᵖ) :
    ((CategoryTheory.Equivalence.sheafCongrPreregular e A).unitIso.hom.app X✝).val.app X = X✝.val.map (e.unitIso.inv.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ᵒᵖ), ((CategoryTheory.Equivalence.sheafCongrPreregular e A).inverse.map f).val.app X_1 = f.val.app (Opposite.op (e.functor.obj X_1.unop))
    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), ((CategoryTheory.Equivalence.sheafCongrPreregular e 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ᵒᵖ), ((CategoryTheory.Equivalence.sheafCongrPreregular e A).functor.map f).val.app X_1 = f.val.app (Opposite.op (e.inverse.obj X_1.unop))
    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] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_6, u_3} A] :
    CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A ≌ CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A

    Equivalent preregular categories give equivalent regular toposes.

    Equations
    Instances For
      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_6, u_2} D] (e : C ≌ D) [CategoryTheory.Preregular C] (A : Type u_3) [CategoryTheory.Category.{u_5, u_3} A] (F : CategoryTheory.Functor Cᵒᵖ A) :
      CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology D) (CategoryTheory.Functor.comp e.inverse.op 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.Functor.comp (CategoryTheory.equivSmallModel C).inverse.op F)

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