feat: define singular `n`-manifolds #15906

grunweg · 2024-08-17T01:19:41Z

These are used to define bordism groups: the n-bordism group of a topological space X is the space of cobordism classes of all singular n-manifolds on X.

This PR can be seen in context in this branch.
I am not sure about the last commit: it silences the checkUnivs linter, but the fall-out elsewhere is not exactly pretty.

github-actions · 2024-08-17T01:20:21Z

PR summary 3cb89c328a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Geometry.Manifold.Bordisms`	1557

Declarations diff

+ SingularNManifold
+ comap
+ comap_f
+ empty
+ instance {n : ℕ} {s : SingularNManifold X n} : BoundarylessManifold s.model s.M := s.boundaryless
+ instance {n : ℕ} {s : SingularNManifold X n} : ChartedSpace s.H s.M := s.chartedSpace
+ instance {n : ℕ} {s : SingularNManifold X n} : CompactSpace s.M := s.compactSpace
+ instance {n : ℕ} {s : SingularNManifold X n} : FiniteDimensional ℝ s.E := s.findim
+ instance {n : ℕ} {s : SingularNManifold X n} : NormedAddCommGroup s.E := s.normedAddCommGroup
+ instance {n : ℕ} {s : SingularNManifold X n} : NormedSpace ℝ s.E := s.normedSpace
+ instance {n : ℕ} {s : SingularNManifold X n} : SmoothManifoldWithCorners s.model s.M := s.smoothMfd
+ instance {n : ℕ} {s : SingularNManifold X n} : TopologicalSpace s.H := s.topSpaceH
+ instance {n : ℕ} {s : SingularNManifold X n} : TopologicalSpace s.M := s.topSpaceM
+ map
+ map_comp
+ map_f
+ prod
+ refl
+ trivial

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

grunweg · 2024-08-18T08:43:25Z

Note to self: merge my improvements to the bordism theory branch here, once the dependent PR has landed.
Update: done now, and cleaned up this PR.

First constructions done; the itneresting ones will require being awake -:-)

…lds. s.f cannot be renamed to map...

alreadydone · 2024-09-07T11:17:14Z

Mathlib/Geometry/Manifold/Bordisms.lean

+  E : Type u
+  /-- `E` is normed (additive) abelian group -/
+  [normedAddCommGroup : NormedAddCommGroup E]
+  /-- `E` is a real normed space -/
+  [normedSpace: NormedSpace ℝ E]
+  /-- The smooth manifold `M` of a singular `n`-manifold `(M,f)` -/
+  M : Type u
+  /-- The smooth manifold `M` is a topological space -/
+  [topSpaceM : TopologicalSpace M]
+  /-- The topological space on which the manifold `M` is modeled -/
+  H : Type u
+  /-- `H` is a topological space -/
+  [topSpaceH : TopologicalSpace H]
+  /-- The smooth manifold `M` is a charted space over `H` -/
+  [chartedSpace : ChartedSpace H M]
+  /-- The model with corners for the manifold `M` -/
+  model : ModelWithCorners ℝ E H
+  /-- `M` is a smooth manifold with corners -/
+  [smoothMfd : SmoothManifoldWithCorners model M]
+  /-- `M` is compact -/
+  [compactSpace : CompactSpace M]
+  /-- `M` is boundaryless -/
+  [boundaryless: BoundarylessManifold model M]
+  /-- `M` is finite-dimensional, as its model space `E` is -/
+  [findim: FiniteDimensional ℝ E]
+  /-- `M` is `n`-dimensional, as its model space `E` is -/
+  [dimension : finrank ℝ E = n]


I'd suggest that you use EuclideanSpace ℝ n and get rid of E and H.

This makes speaking about products more difficult: when talking about products of bordism classes and the (un)oriented bordism ring, that would be needed. Why would you use euclidean space instead?

YaelDillies · 2024-10-31T15:42:20Z

Mathlib/Geometry/Manifold/Bordisms.lean

+  /-- `M` is finite-dimensional, as its model space `E` is -/
+  [findim: FiniteDimensional ℝ E]
+  /-- `M` is `n`-dimensional, as its model space `E` is -/
+  [dimension : finrank ℝ E = n]


This is not a class, right? How does Lean even accept it?

Suggested change

[dimension : finrank ℝ E = n]

dimension : finrank ℝ E = n

sgouezel

Can you sketch a little bit more the maths behind this, which I don't know? (For me, a cobordism between two manifolds M and N is a manifold one dimension higher with two boundary components which are diffeomorphic to M and N respectively, but I don't see how your singular manifolds fit into this picture). Either in the file-level docstring, or in the PR, as you prefer.

I think it would help me a lot to see a theorem which is proved with this formalism (the proof of the pudding is in the eating). Do you have a working branch with a specific theorem you could point me to, so that I get a better grasp of where you want to go? (Ideally you could even open a PR with a work in progress branch, for easier discussion there)

sgouezel · 2024-10-31T17:34:55Z

Mathlib/Geometry/Manifold/Bordisms.lean

+of a closed `n`-dimensional smooth manifold `M` together with a continuous map `M → X`. -/
+structure SingularNManifold (X : Type*) [TopologicalSpace X] (n : ℕ) where
+  /-- The normed space on which the manifold `M` is modeled. -/
+  E : Type u


I don't think it can be correct to assume that E lives in the same universe as M: typically, I expect M to live in a generic universe, while E would be R^n (living in Type). So your definition should probably depend on two universes u (for M) and v (for E and H)?

sgouezel · 2024-10-31T17:35:09Z

Mathlib/Geometry/Manifold/Bordisms.lean

+## Main definitions
+
+- **SingularNManifold**: a singular `n`-manifold on a topological space `X`, for `n ∈ ℕ`, is a pair
+`(M,f)` of a closed `n`-dimensional smooth manifold `M` together with a continuous map `M → X`.


Suggested change

`(M,f)` of a closed `n`-dimensional smooth manifold `M` together with a continuous map `M → X`.

`(M, f)` of a closed `n`-dimensional smooth manifold `M` together with a continuous map `M → X`.

sgouezel · 2024-10-31T17:36:39Z

Mathlib/Geometry/Manifold/Bordisms.lean

+  /-- The smooth manifold `M` is a charted space over `H` -/
+  [chartedSpace : ChartedSpace H M]
+  /-- The model with corners for the manifold `M` -/
+  model : ModelWithCorners ℝ E H


Maybe call it I instead of model, to follow the convention in the rest of the library?

sgouezel · 2024-10-31T17:38:00Z

Mathlib/Geometry/Manifold/Bordisms.lean

+a smooth map `φ : M → N` induces a singular `n`-manifold structure `(M, f ∘ φ)` on `X`. -/
+noncomputable def comap [h: Fact (finrank ℝ E = n)]
+    (s : SingularNManifold X n)
+    {φ : M → s.M} (hφ : Smooth I s.model φ) : SingularNManifold X n where


It's a little bit strange to assume that phi is smooth, while continuous would do here, no?

sgouezel · 2024-10-31T17:38:14Z

Mathlib/Geometry/Manifold/Bordisms.lean

+
+/-- If `(N, f)` is a singular `n`-manifold on `X` and `M` another `n`-dimensional smooth manifold,
+a smooth map `φ : M → N` induces a singular `n`-manifold structure `(M, f ∘ φ)` on `X`. -/
+noncomputable def comap [h: Fact (finrank ℝ E = n)]


Suggested change

noncomputable def comap [h: Fact (finrank ℝ E = n)]

noncomputable def comap [h : Fact (finrank ℝ E = n)]

Same thing below

sgouezel · 2024-10-31T17:39:16Z

Mathlib/Geometry/Manifold/Bordisms.lean

+  f := fun _ ↦ PUnit.unit
+  hf := continuous_const
+
+/-- The product of a singular `n`- and a `m`-manifold into a one-point space


Suggested change

/-- The product of a singular `n`- and a `m`-manifold into a one-point space

/-- The product of a singular `n`- and a singular `m`-manifold into a one-point space

sgouezel · 2024-10-31T17:39:28Z

Mathlib/Geometry/Manifold/Bordisms.lean

+
+/-- The product of a singular `n`- and a `m`-manifold into a one-point space
+is a singular `n+m`-manifold. -/
+-- FUTURE: prove that this observation inducess a commutative ring structure


Suggested change

-- FUTURE: prove that this observation inducess a commutative ring structure

-- FUTURE: prove that this observation induces a commutative ring structure

grunweg added the t-differential-geometry Manifolds etc label Aug 17, 2024

grunweg force-pushed the MR-singular-nmanifolds branch from 0a0da6b to 85f4ff6 Compare August 17, 2024 01:21

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Aug 17, 2024

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Sep 3, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 3, 2024

grunweg added 2 commits September 3, 2024 22:55

Change

f70927a

Small tweaks.

01ae66b

grunweg force-pushed the MR-singular-nmanifolds branch from 85f4ff6 to 01ae66b Compare September 3, 2024 21:09

WIP: move data into singularnmanifold

1fa6a50

First constructions done; the itneresting ones will require being awake -:-)

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 3, 2024

grunweg added 3 commits September 4, 2024 10:58

Further: rename old variant to be clearly deprecated; rename some fie…

bb1c5e4

…lds. s.f cannot be renamed to map...

wip: further; enough for now

e96f6a2

Fix proofs: just comap ones remaining.

0ad05d3

leanprover-community deleted a comment from leanprover-community-mathlib4-bot Sep 6, 2024

grunweg added 3 commits September 6, 2024 22:48

Last edits, and add a docstring.

71196a5

Add lots of documentation.

0832a19

RFC: fix checkUnivs linter

3cb89c3

alreadydone reviewed Sep 7, 2024

View reviewed changes

YaelDillies reviewed Oct 31, 2024

View reviewed changes

sgouezel reviewed Oct 31, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: define singular `n`-manifolds #15906

feat: define singular `n`-manifolds #15906

grunweg commented Aug 17, 2024 •

edited

Loading

github-actions bot commented Aug 17, 2024 •

edited

Loading

Declarations diff

grunweg commented Aug 18, 2024 •

edited

Loading

alreadydone Sep 7, 2024

grunweg Sep 9, 2024

YaelDillies Oct 31, 2024

sgouezel left a comment •

edited

Loading

sgouezel Oct 31, 2024

sgouezel Oct 31, 2024

sgouezel Oct 31, 2024

sgouezel Oct 31, 2024

sgouezel Oct 31, 2024

sgouezel Oct 31, 2024

sgouezel Oct 31, 2024

	[dimension : finrank ℝ E = n]
	dimension : finrank ℝ E = n

	`(M,f)` of a closed `n`-dimensional smooth manifold `M` together with a continuous map `M → X`.
	`(M, f)` of a closed `n`-dimensional smooth manifold `M` together with a continuous map `M → X`.

	noncomputable def comap [h: Fact (finrank ℝ E = n)]
	noncomputable def comap [h : Fact (finrank ℝ E = n)]

	/-- The product of a singular `n`- and a `m`-manifold into a one-point space
	/-- The product of a singular `n`- and a singular `m`-manifold into a one-point space

	-- FUTURE: prove that this observation inducess a commutative ring structure
	-- FUTURE: prove that this observation induces a commutative ring structure

feat: define singular n-manifolds #15906

Are you sure you want to change the base?

feat: define singular n-manifolds #15906

Conversation

grunweg commented Aug 17, 2024 • edited Loading

github-actions bot commented Aug 17, 2024 • edited Loading

PR summary 3cb89c328a

Import changes for modified files

Declarations diff

grunweg commented Aug 18, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sgouezel left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

feat: define singular `n`-manifolds #15906

feat: define singular `n`-manifolds #15906

grunweg commented Aug 17, 2024 •

edited

Loading

github-actions bot commented Aug 17, 2024 •

edited

Loading

grunweg commented Aug 18, 2024 •

edited

Loading

sgouezel left a comment •

edited

Loading