CategoryTheory.GrothendieckTopology.plusMap_comp
theorem CategoryTheory.GrothendieckTopology.plusMap_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D]
[inst_2 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
[inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R),
J.plusMap (CategoryTheory.CategoryStruct.comp η γ) =
CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.plusMap γ)
The theorem `CategoryTheory.GrothendieckTopology.plusMap_comp` states that for any Grothendieck topology `J` in a category `C` and categories `D`, given functors `P`, `Q`, and `R` from the opposite of `C` to `D`, and morphisms `η` from `P` to `Q` and `γ` from `Q` to `R`, the `plusMap` operation with respect to the Grothendieck topology `J` on the composition of `η` and `γ` is equivalent to the composition of the `plusMap` operation on `η` and the `plusMap` operation on `γ`. This is assuming that for each object `X` in `C` and cover `S` of `X` with respect to `J`, the cover index has a multiequalizer, and `X` has colimits of shape given by the opposite of the cover of `X`. In essence, this theorem demonstrates the compatibility of the `plusMap` operation with the composition of morphisms.
More concisely: Given a Grothendieck topology `J` on a category `C` and functors `P`, `Q`, `R` from `C^op` to another category `D` with cover index multiequalizers and colimits, the `plusMap` of `γ ∘ η` is equivalent to the composition of `plusMap η` and `plusMap γ`.
|
CategoryTheory.GrothendieckTopology.diagram.proof_1
theorem CategoryTheory.GrothendieckTopology.diagram.proof_1 :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
{D : Type u_3} [inst_1 : CategoryTheory.Category.{max u_2 u_1, u_3} D]
[inst_2 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
(P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : (J.Cover X)ᵒᵖ),
CategoryTheory.Limits.HasMultiequalizer (S.unop.index P)
This theorem, `CategoryTheory.GrothendieckTopology.diagram.proof_1`, states that for any category `C` with a Grothendieck topology `J`, and any category `D`, if every functor from the opposite category of `C` to `D` has a multi-equalizer for every cover `S` of any object `X` in `C` (this cover being a poset with respect to the Grothendieck topology `J`), then for any such functor `P` and any such cover `S` (taken in the opposite category), the multi-equalizer exists for the index of the cover `S` with respect to the functor `P`.
More concisely: If every functor from the opposite category of a category with a Grothendieck topology has a multi-equalizer for every cover, then the multi-equalizer for the index of any cover with respect to such a functor exists.
|
CategoryTheory.GrothendieckTopology.plusObj.proof_1
theorem CategoryTheory.GrothendieckTopology.plusObj.proof_1 :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
{D : Type u_3} [inst_1 : CategoryTheory.Category.{max u_2 u_1, u_3} D]
[inst_2 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
(P : CategoryTheory.Functor Cᵒᵖ D) [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
(X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (J.diagram P X.unop)
The theorem `CategoryTheory.GrothendieckTopology.plusObj.proof_1` states that for any category `C` (with a given Grothendieck topology `J`) and category `D`, if for every contravariant functor `P` from `C` to `D`, every object `X` in `C`, and every cover `S` of `X` with respect to the Grothendieck topology `J`, the multicospan indexed by the cover `S` and the functor `P` has a limit (i.e., it has a multiequalizer), and if for every object `X` in `C`, the category `D` has colimits of shape given by the opposite category of the poset of `J`-covers of `X`, then for any contravariant functor `P` from `C` to `D` and any object `X` in the opposite category of `C`, the diagram in `D` given by `J` and `P` for the object `X` unop has a colimit. In simpler terms, this theorem asserts the existence of certain colimits in the category `D` under specific conditions related to the functor `P` and the Grothendieck topology `J`.
More concisely: Given a category C with a Grothendieck topology J, and a contravariant functor P from C to D, if for every cover S of an object X in C and every P(x), the multicospan has a limit, and D has colimits of shape given by the opposite category of J-covers, then the diagram given by J and P for any object X' in the opposite category of C has a colimit in D.
|
CategoryTheory.GrothendieckTopology.plusMap_toPlus
theorem CategoryTheory.GrothendieckTopology.plusMap_toPlus :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D]
[inst_2 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
(P : CategoryTheory.Functor Cᵒᵖ D) [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D],
J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P)
This theorem in the context of category theory and Grothendieck topologies asserts that for any category `C` and a Grothendieck topology `J` on `C`, and any category `D` such that for any functor `P` from the opposite of `C` to `D`, any object `X` in `C`, and any cover `S` of `X` in `J`, the multicospan indexed by the cover of `X` with respect to the functor `P` has a multiequalizer, and the category `D` has all colimits of shape opposite to the poset of covers of `X` in `J` for any `X` in `C`. The plus construction applied to the morphism from `P` to its plus construction is equal to the morphism from the plus construction of `P` to the plus construction applied twice to `P`. This means, in the notation used in the theorem, `(P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺`.
More concisely: For any category `C` with a Grothendieck topology `J`, and any functor `P` from the opposite of `C` to a category `D` with all colimits, the multiequalizer of the multicospan defined by `P` and the cover relations in `J` exists, and the plus construction preserves the identity morphism up to composition with `P`: `(P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺`.
|
CategoryTheory.GrothendieckTopology.toPlus_naturality
theorem CategoryTheory.GrothendieckTopology.toPlus_naturality :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D]
[inst_2 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
[inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q),
CategoryTheory.CategoryStruct.comp η (J.toPlus Q) =
CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusMap η)
The theorem `CategoryTheory.GrothendieckTopology.toPlus_naturality` states that for a category `C` with a Grothendieck topology `J`, another category `D`, and two functors `P` and `Q` from the opposite of `C` to `D`, when we have certain structures in place (specifically, for any object `X` in `C` and any cover `S` of `X` in `J`, the multicospan associated with the index of the cover on `P` has a limit, and any object `X` in `C` has colimits of shape opposite to the poset of covers of `X` in `D`), then the composition of a morphism `η` from `P` to `Q` with the `toPlus` operation on `Q` (according to `J`) equals the composition of the `toPlus` operation on `P` (according to `J`) with the `plusMap` operation on `η` (according to `J`). In other words, this theorem shows the naturality of the `toPlus` operation in the context of the Grothendieck topology.
More concisely: Given a category with a Grothendieck topology, for any two functors from the opposite category with the required structures, the `toPlus` operation on their composite is equal to the composition of the `toPlus` operations and the `plusMap` operation.
|
CategoryTheory.GrothendieckTopology.plusLift_unique
theorem CategoryTheory.GrothendieckTopology.plusLift_unique :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
[inst_1 : CategoryTheory.Category.{max v u, w} D]
[inst_2 :
∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
CategoryTheory.Limits.HasMultiequalizer (S.index P)]
[inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
{P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : J.plusObj P ⟶ Q),
CategoryTheory.CategoryStruct.comp (J.toPlus P) γ = η → γ = J.plusLift η hQ
The theorem `CategoryTheory.GrothendieckTopology.plusLift_unique` in Lean 4 states that for any categories `C` and `D`, Grothendieck topology `J` on `C`, functors `P` and `Q` from the opposite of `C` to `D`, and a natural transformation `η` from `P` to `Q`, if `Q` is a sheaf with respect to `J`, and there exists a morphism `γ` from the plus construction of `P` with respect to `J` to `Q` such that the composition of the morphism from `P` to the plus construction of `P` with `γ` equals `η`, then `γ` must be the lift of `η` via the plus construction of `J`. This theorem asserts the uniqueness of the lift in the particular context of the plus construction in Grothendieck topologies. The plus construction is a way of associating a sheaf to a presheaf in a Grothendieck topology.
More concisely: Given categories C, D, a Grothendieck topology J on C, functors P and Q from the opposite of C to D, and a natural transformation η from P to Q with Q being a sheaf and having a morphism γ from the plus construction of P with respect to J to Q such that the composite of the morphism from P to the plus construction of P and γ equals η, then γ is the unique lift of η via the plus construction of J.
|