From 1dc9339a6c55a095b29cf84637055608608be1b6 Mon Sep 17 00:00:00 2001 From: grunweg Date: Thu, 18 Apr 2024 08:21:44 +0000 Subject: [PATCH] doc(Manifold/Charted): document the fields of `Pregroupoid` (#11930) Similar to #9827. --- Mathlib/Geometry/Manifold/ChartedSpace.lean | 7 +++++++ scripts/nolints.json | 1 - 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean index 6ececb636dfbf..ad4a0cafb8aba 100644 --- a/Mathlib/Geometry/Manifold/ChartedSpace.lean +++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean @@ -342,12 +342,19 @@ both the function and its inverse have some property. If this property is stable one gets a groupoid. `Pregroupoid` bundles the properties needed for this construction, with the groupoid of smooth functions with smooth inverses as an application. -/ structure Pregroupoid (H : Type*) [TopologicalSpace H] where + /-- Property describing membership in this groupoid: the pregroupoid "contains" + all functions `H → H` having the pregroupoid property on some `s : Set H` -/ property : (H → H) → Set H → Prop + /-- The pregroupoid property is stable under composition -/ comp : ∀ {f g u v}, property f u → property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → property (g ∘ f) (u ∩ f ⁻¹' v) + /-- Pregroupoids contain the identity map (on `univ`) -/ id_mem : property id univ + /-- The pregroupoid property is "local", in the sense that `f` has the pregroupoid property on `u` + iff its restriction to each open subset of `u` has it -/ locality : ∀ {f u}, IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ property f (u ∩ v)) → property f u + /-- If `f = g` on `u` and `property f u`, then `property g u` -/ congr : ∀ {f g : H → H} {u}, IsOpen u → (∀ x ∈ u, g x = f x) → property f u → property g u #align pregroupoid Pregroupoid diff --git a/scripts/nolints.json b/scripts/nolints.json index a6ce393295fd4..694b621ae71e0 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -337,7 +337,6 @@ ["docBlame", "PowerBasis.basis"], ["docBlame", "PowerBasis.dim"], ["docBlame", "PowerBasis.gen"], - ["docBlame", "Pregroupoid.property"], ["docBlame", "PresheafOfModules.presheaf"], ["docBlame", "Pretrivialization.baseSet"], ["docBlame", "PrimeSpectrum.asIdeal"],