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.

@[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 (Opposite.unop X)).op
@[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 (Opposite.unop X)).op
@[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
@[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
@[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 (Opposite.unop X)).op
@[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 (Opposite.op (e.functor.obj (Opposite.unop X_1)))
@[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 (Opposite.unop X)).op
@[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 (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
@[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
@[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 (Opposite.unop X)).op
@[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 (Opposite.unop X)).op
@[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
@[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 (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
@[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 (Opposite.unop X)).op
@[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 (Opposite.op (e.functor.obj (Opposite.unop X_1)))
@[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ᵒᵖ) :
((e.sheafCongrPreregular A).counitIso.inv.app X✝).val.app X = X✝.val.map (e.counitIso.hom.app (Opposite.unop X)).op