TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck
theorem TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck :
∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X) (R : CategoryTheory.Presieve U),
CategoryTheory.Sieve.generate R ∈ (Opens.grothendieckTopology ↑X).sieves U →
iSup (TopCat.Presheaf.coveringOfPresieve U R) = U
This theorem asserts that for any topological space `X`, open set `U` within `X`, and a presieve `R` on `U`, if the sieve generated from `R` is included in the Grothendieck topology on the open sets of `X` at `U`, then the supremum of the covering family associated with `R` equals `U`. In other words, if `R` is a presieve in the Grothendieck topology on the open sets of `X`, the covering family associated to `R` indeed covers `U`, i.e., the union of all open sets in the covering family equals `U`.
More concisely: Given a topological space X, an open set U, and a presieve R on U in the Grothendieck topology such that the sieve generated by R is contained in the Grothendieck topology at U, the supremum of the covering family associated with R equals U.
|
TopCat.Presheaf.covering_presieve_eq_self
theorem TopCat.Presheaf.covering_presieve_eq_self :
∀ {X : TopCat} {Y : TopologicalSpace.Opens ↑X} (R : CategoryTheory.Presieve Y),
TopCat.Presheaf.presieveOfCoveringAux (TopCat.Presheaf.coveringOfPresieve Y R) Y = R
This theorem states that for any topological space `X` and any open set `Y` in `X`, given a presieve `R` on `Y`, if we first construct a family of open sets using the function `coveringOfPresieve` with `R` as an input (which may not necessarily cover `Y` if `R` isn't a covering), and then construct a new presieve on `Y` using this family of open sets via the function `presieveOfCoveringAux`, we will end up with the original presieve `R`. In other words, the operations of constructing a family of open sets from a presieve and then constructing a presieve from this family are inverses of each other, as long as we start with a presieve.
More concisely: Given any topological space `X`, open set `Y` in `X`, and presieve `R` on `Y`, the functions `coveringOfPresieve` and `presieveOfCoveringAux` are inverses of each other when applied to `R`.
|
TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology
theorem TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology :
∀ {X : TopCat} {ι : Type v} (U : ι → TopologicalSpace.Opens ↑X),
CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCovering U) ∈
(Opens.grothendieckTopology ↑X).sieves (iSup U)
The theorem `TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology` states that for any topological space `X` within the category of topological spaces `TopCat` and for any indexed family of open subsets `U` of `X`, the sieve generated by the presieve associated with the covering `U` is a member of the Grothendieck topology of `X`. This is evaluated at the indexed supremum (iSup) of `U`. In simpler terms, this theorem relates the notions of a covering of a topological space, the corresponding presieve, the generation of a sieve from that presieve, and its membership in the Grothendieck topology of the space.
More concisely: For any topological space X in TopCat and indexed family U of open subsets of X, the sieve generated by the presheaf of a covering U is in the Grothendieck topology of X.
|