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

Precoherent is preserved by equivalence of categories.

source
instance CategoryTheory.Equivalence.instPrecoherentSmallModel {C : Type u_1} [Category.{u_4, u_1} C] [Precoherent C] [EssentiallySmall.{u_3, u_4, u_1} C] :
Precoherent (SmallModel.{u_3, u_4, u_1} C)
source
instance CategoryTheory.Equivalence.instIsDenseSubsiteCoherentTopologyInverse {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] [Precoherent C] (e : C ≌ D) :
Functor.IsDenseSubsite (coherentTopology D) (coherentTopology C) e.inverse
source
def CategoryTheory.Equivalence.sheafCongrPrecoherent {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) :
Sheaf (coherentTopology C) A ≌ Sheaf (coherentTopology D) A

Equivalent precoherent categories give equivalent coherent toposes.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (X : Sheaf (coherentTopology D) A) (X✝ : Dᵒᵖ) :
    ((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_unitIso_inv_app_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (X : Sheaf (coherentTopology C) A) (X✝ : Cᵒᵖ) :
    ((sheafCongrPrecoherent A e).unitIso.inv.app X).val.app X✝ = X.val.map (e.unitIso.hom.app (Opposite.unop X✝)).op
    source
    @[simp]
    theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (X : Sheaf (coherentTopology C) A) (X✝ : Cᵒᵖ) :
    ((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_obj_val_map {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Sheaf (coherentTopology D) A) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) :
    ((sheafCongrPrecoherent A e).inverse.obj F).val.map f = F.val.map (e.functor.map f.unop).op
    source
    @[simp]
    theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) {X✝ Y✝ : Sheaf (coherentTopology C) A} (f : X✝ ⟶ Y✝) (X : Dᵒᵖ) :
    ((sheafCongrPrecoherent A e).functor.map f).val.app X = f.val.app (Opposite.op (e.inverse.obj (Opposite.unop X)))
    source
    @[simp]
    theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) {X✝ Y✝ : Sheaf (coherentTopology D) A} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) :
    ((sheafCongrPrecoherent A e).inverse.map f).val.app X = f.val.app (Opposite.op (e.functor.obj (Opposite.unop X)))
    source
    @[simp]
    theorem CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_val_obj {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Sheaf (coherentTopology C) A) (X : Dᵒᵖ) :
    ((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} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (X : Sheaf (coherentTopology D) A) (X✝ : Dᵒᵖ) :
    ((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_obj_val_map {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Sheaf (coherentTopology C) A) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) :
    ((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} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Sheaf (coherentTopology D) A) (X : Cᵒᵖ) :
    ((sheafCongrPrecoherent A e).inverse.obj F).val.obj X = F.val.obj (Opposite.op (e.functor.obj (Opposite.unop X)))
    source
    theorem CategoryTheory.Equivalence.precoherent_isSheaf_iff {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Functor Cᵒᵖ A) :
    Presheaf.IsSheaf (coherentTopology C) F ↔ Presheaf.IsSheaf (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} [Category.{u_5, u_1} C] [Precoherent C] (A : Type u_3) [Category.{u_6, u_3} A] [EssentiallySmall.{u_4, u_5, u_1} C] (F : Functor Cᵒᵖ A) :
    Presheaf.IsSheaf (coherentTopology C) F ↔ Presheaf.IsSheaf (coherentTopology (SmallModel.{u_4, u_5, u_1} C)) ((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} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] [Preregular C] (e : C ≌ D) :
    Preregular D

    Preregular is preserved by equivalence of categories.

    source
    instance CategoryTheory.Equivalence.instPreregularSmallModel {C : Type u_1} [Category.{u_4, u_1} C] [Preregular C] [EssentiallySmall.{u_3, u_4, u_1} C] :
    Preregular (SmallModel.{u_3, u_4, u_1} C)
    source
    instance CategoryTheory.Equivalence.instIsDenseSubsiteRegularTopologyInverse {C : Type u_1} [Category.{u_3, u_1} C] {D : Type u_2} [Category.{u_4, u_2} D] [Preregular C] (e : C ≌ D) :
    Functor.IsDenseSubsite (regularTopology D) (regularTopology C) e.inverse
    source
    def CategoryTheory.Equivalence.sheafCongrPreregular {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) :
    Sheaf (regularTopology C) A ≌ Sheaf (regularTopology D) A

    Equivalent preregular categories give equivalent regular toposes.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Equivalence.sheafCongrPreregular_functor_map_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) {X✝ Y✝ : Sheaf (regularTopology C) A} (f : X✝ ⟶ Y✝) (X : Dᵒᵖ) :
      ((sheafCongrPreregular A e).functor.map f).val.app X = f.val.app (Opposite.op (e.inverse.obj (Opposite.unop X)))
      source
      @[simp]
      theorem CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (X : Sheaf (regularTopology D) A) (X✝ : Dᵒᵖ) :
      ((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_inverse_obj_val_obj {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Sheaf (regularTopology D) A) (X : Cᵒᵖ) :
      ((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} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (X : Sheaf (regularTopology C) A) (X✝ : Cᵒᵖ) :
      ((sheafCongrPreregular A e).unitIso.inv.app X).val.app X✝ = X.val.map (e.unitIso.hom.app (Opposite.unop X✝)).op
      source
      @[simp]
      theorem CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_val_obj {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Sheaf (regularTopology C) A) (X : Dᵒᵖ) :
      ((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_inverse_obj_val_map {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Sheaf (regularTopology D) A) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) :
      ((sheafCongrPreregular A e).inverse.obj F).val.map f = F.val.map (e.functor.map f.unop).op
      source
      @[simp]
      theorem CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (X : Sheaf (regularTopology C) A) (X✝ : Cᵒᵖ) :
      ((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_inverse_map_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) {X✝ Y✝ : Sheaf (regularTopology D) A} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) :
      ((sheafCongrPreregular A e).inverse.map f).val.app X = f.val.app (Opposite.op (e.functor.obj (Opposite.unop X)))
      source
      @[simp]
      theorem CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_val_map {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Sheaf (regularTopology C) A) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) :
      ((sheafCongrPreregular A e).functor.obj F).val.map f = F.val.map (e.inverse.map f.unop).op
      source
      @[simp]
      theorem CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_val_app {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (X : Sheaf (regularTopology D) A) (X✝ : Dᵒᵖ) :
      ((sheafCongrPreregular A e).counitIso.inv.app X).val.app X✝ = X.val.map (e.counitIso.hom.app (Opposite.unop X✝)).op
      source
      theorem CategoryTheory.Equivalence.preregular_isSheaf_iff {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] (e : C ≌ D) (F : Functor Cᵒᵖ A) :
      Presheaf.IsSheaf (regularTopology C) F ↔ Presheaf.IsSheaf (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} [Category.{u_5, u_1} C] [Preregular C] (A : Type u_3) [Category.{u_6, u_3} A] [EssentiallySmall.{u_4, u_5, u_1} C] (F : Functor Cᵒᵖ A) :
      Presheaf.IsSheaf (regularTopology C) F ↔ Presheaf.IsSheaf (regularTopology (SmallModel.{u_4, u_5, u_1} C)) ((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.