G-topologies and their sites

A G-topology specifies admissible covers of a meet-closed family of subsets, without requiring arbitrary unions to be admissible. Its covers are set-theoretic covers, stable under restriction and composition. We use an order embedding into the subsets of the underlying space so that the same construction applies to bundled admissible opens as well as subtypes of sets.

GTopology.grothendieckTopology constructs the site on the inclusion preorder of admissible opens. GTopology.isSheaf_iff identifies its sheaves with presheaves satisfying unique gluing on admissible covers, using Mathlib's matching families and sheaf categories throughout. A monotone map of admissible opens that sends admissible covers to admissible covers gives a cover-preserving functor of sites (GTopology.coverPreserving_functor). GTopology.topological recovers ordinary open covers, and its site is the usual open-set site.

A G-topology is saturated (GTopology.Saturated) if it satisfies the conditions (G0)–(G2) of [BGR, §9.1.2]: the empty set is admissible, admissibility of a subset can be checked on the members of an admissible cover, and a covering by admissible opens is admissible as soon as it is refined by an admissible cover. The G-topology of ordinary open covers is saturated (GTopology.saturated_topological). Admissibility of a covering family is local on an admissible cover (GTopology.Saturated.covers_iff_restriction), and a family containing an admissible cover is admissible (GTopology.Saturated.covers_of_superset). The admissible opens of any G-topology form a basis of the topology they generate (GTopology.isTopologicalBasis_range).

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §§9.1.1 and 9.1.2.

structure TauCeti.GTopology {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] (ι : B ↪o Set X) : Type v

Admissible covers on a family of subsets closed under finite intersections and containing the whole space. The family is represented by an order embedding ι, preserving intersections and the largest open. Covering families are sets, so repetitions and indexing choices carry no additional data.

• map_top : ι ⊤ = Set.univ

  The largest admissible open is the whole space.

• map_inf (U V : B) : ι (U ⊓ V) = ι U ∩ ι V

  Meets represent intersections.

• Covers : B → Set B → Prop

  The predicate of admissible covering families.

• subset {U : B} {S : Set B} : self.Covers U S → ∀ V ∈ S, V ≤ U

  Every member of a cover is contained in its target.

• union_eq {U : B} {S : Set B} : self.Covers U S → ⋃₀ (⇑ι '' S) = ι U

  An admissible cover covers the underlying set.

• identity (U : B) : self.Covers U {U}

  Identity covers are admissible.

• restriction {U : B} {S : Set B} : self.Covers U S → ∀ V ≤ U, self.Covers V ((fun (W : B) => W ⊓ V) '' S)

  Restricting an admissible cover by intersection is admissible.

• transitive {U : B} {S : Set B} {T : B → Set B} : self.Covers U S → (∀ V ∈ S, self.Covers V (T V)) → self.Covers U (⋃ V ∈ S, T V)

  Composing admissible covers gives an admissible cover.

theorem TauCeti.GTopology.ext_iff {X : Type u} {B : Type v} {inst✝ : SemilatticeInf B} {inst✝¹ : OrderTop B} {ι : B ↪o Set X} {x y : GTopology ι} : x = y ↔ x.Covers = y.Covers

theorem TauCeti.GTopology.ext {X : Type u} {B : Type v} {inst✝ : SemilatticeInf B} {inst✝¹ : OrderTop B} {ι : B ↪o Set X} {x y : GTopology ι} (Covers : x.Covers = y.Covers) : x = y

def TauCeti.GTopology.coverPresieve {B : Type v} [Preorder B] (U : B) (S : Set B) : CategoryTheory.Presieve U

The presieve whose arrows are the inclusions of members of S into U.

@[simp]

theorem TauCeti.GTopology.coverPresieve_apply {B : Type v} [Preorder B] {U V : B} (S : Set B) (f : V ⟶ U) : coverPresieve U S f ↔ V ∈ S

structure TauCeti.GTopology.Saturated {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} (G : GTopology ι) : Prop

A G-topology is saturated if it satisfies the conditions (G0)–(G2) of [BGR, §9.1.2]. The whole space is always admissible, so (G0) only asks for the empty set.

• empty_mem_range : ∅ ∈ Set.range ⇑ι

  (G0) The empty set is admissible.

• mem_range_of_covers {U : B} {S : Set B} : G.Covers U S → ∀ V ⊆ ι U, (∀ W ∈ S, V ∩ ι W ∈ Set.range ⇑ι) → V ∈ Set.range ⇑ι

  (G1) A subset of an admissible open whose intersections with the members of an admissible cover are admissible is itself admissible.

• covers_of_refinement {U : B} {S R : Set B} : ⋃₀ (⇑ι '' S) = ι U → G.Covers U R → (∀ W ∈ R, ∃ W' ∈ S, W ≤ W') → G.Covers U S

  (G2) A covering of an admissible open by admissible opens is admissible if some admissible cover refines it.

theorem TauCeti.GTopology.Saturated.covers_of_superset {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} {G : GTopology ι} (hG : G.Saturated) {U : B} {R S : Set B} (hR : G.Covers U R) (hRS : R ⊆ S) (hS : ∀ W ∈ S, W ≤ U) : G.Covers U S

In a saturated G-topology, a family of admissible opens contained in U is an admissible cover of U as soon as it contains one.

theorem TauCeti.GTopology.Saturated.covers_iff_restriction {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} {G : GTopology ι} (hG : G.Saturated) {U V : B} {C S : Set B} (hC : G.Covers U C) (hVU : V ≤ U) : G.Covers V S ↔ (∀ W ∈ S, W ≤ V) ∧ ∀ W ∈ C, G.Covers (V ⊓ W) ((fun (Z : B) => Z ⊓ W) '' S)

In a saturated G-topology, a family of admissible opens contained in V covers V admissibly if and only if it does so after intersection with each member of an admissible cover of an ambient open U.

theorem TauCeti.GTopology.isTopologicalBasis_range {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} (G : GTopology ι) : TopologicalSpace.IsTopologicalBasis (Set.range ⇑ι)

The admissible opens of G form a basis of the topology they generate.

theorem TauCeti.GTopology.isOpen_generateFrom_range_iff {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} (G : GTopology ι) {V : Set X} : IsOpen V ↔ ∀ x ∈ V, ∃ (U : B), x ∈ ι U ∧ ι U ⊆ V

The open sets of the topology generated by the admissible opens are the unions of admissible opens.

def TauCeti.GTopology.coverage {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} (G : GTopology ι) : CategoryTheory.Coverage B

Admissible covers give a coverage on the preorder of admissible opens.

@[simp]

theorem TauCeti.GTopology.mem_coverage_iff {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} (G : GTopology ι) {U : B} {R : CategoryTheory.Presieve U} : R ∈ G.coverage.coverings U ↔ ∃ (S : Set B), G.Covers U S ∧ R = coverPresieve U S

noncomputable def TauCeti.GTopology.grothendieckTopology {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} (G : GTopology ι) : CategoryTheory.GrothendieckTopology B

The site on admissible opens: a sieve covers if it contains an admissible cover.

theorem TauCeti.GTopology.mem_grothendieckTopology_iff {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} (G : GTopology ι) {U : B} {R : CategoryTheory.Sieve U} : R ∈ G.grothendieckTopology U ↔ ∃ (S : Set B), G.Covers U S ∧ coverPresieve U S ≤ R.arrows

Covering sieves are exactly those containing an admissible cover.

theorem TauCeti.GTopology.coverage_toGrothendieck {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} (G : GTopology ι) : G.coverage.toGrothendieck = G.grothendieckTopology

The explicit site is generated by the native coverage of admissible covers.

theorem TauCeti.GTopology.isSheaf_iff {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} (G : GTopology ι) (P : CategoryTheory.Functor Bᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheaf G.grothendieckTopology P ↔ ∀ (U : B) (S : Set B), G.Covers U S → CategoryTheory.Presieve.IsSheafFor P (coverPresieve U S)

The site sheaf condition is precisely unique gluing of matching families on all admissible covers. Presieve.IsSheafFor is Mathlib's existence-and-uniqueness condition for amalgamations.

theorem TauCeti.GTopology.coverPreserving_functor {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B] {ι : B ↪o Set X} {G : GTopology ι} {Y : Type u_1} {B' : Type u_2} [SemilatticeInf B'] [OrderTop B'] {ι' : B' ↪o Set Y} {G' : GTopology ι'} {φ : B' → B} (hφ : Monotone φ) (h : ∀ {V : B'} {S : Set B'}, G'.Covers V S → G.Covers (φ V) (φ '' S)) : CategoryTheory.CoverPreserving G'.grothendieckTopology G.grothendieckTopology hφ.functor

A monotone map of admissible opens sending admissible covers to admissible covers induces a cover-preserving functor of the associated sites.

def TauCeti.GTopology.opensEmbedding (Y : Type u) [TopologicalSpace Y] : TopologicalSpace.Opens Y ↪o Set Y

The order embedding sending a bundled open subset to its underlying set.

@[simp]

theorem TauCeti.GTopology.opensEmbedding_apply (Y : Type u) [TopologicalSpace Y] (U : TopologicalSpace.Opens Y) : (opensEmbedding Y) U = ↑U

def TauCeti.GTopology.topological (Y : Type u) [TopologicalSpace Y] : GTopology (opensEmbedding Y)

The G-topology of all ordinary open covers.

@[simp]

theorem TauCeti.GTopology.topological_covers_iff (Y : Type u) [TopologicalSpace Y] {U : TopologicalSpace.Opens Y} {S : Set (TopologicalSpace.Opens Y)} : (topological Y).Covers U S ↔ ⋃₀ ((fun (V : TopologicalSpace.Opens Y) => ↑V) '' S) = ↑U

theorem TauCeti.GTopology.saturated_topological (Y : Type u) [TopologicalSpace Y] : (topological Y).Saturated

The G-topology of ordinary open covers satisfies (G0)–(G2).

theorem TauCeti.GTopology.topological_grothendieckTopology (Y : Type u) [TopologicalSpace Y] : (topological Y).grothendieckTopology = Opens.grothendieckTopology Y

The ordinary topological G-site is Mathlib's open-set site, not a new sheaf category.