-
Notifications
You must be signed in to change notification settings - Fork 331
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: define singular n
-manifolds
#15906
base: master
Are you sure you want to change the base?
Conversation
PR summary 3cb89c328aImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
0a0da6b
to
85f4ff6
Compare
Note to self: merge my improvements to the bordism theory branch here, once the dependent PR has landed. |
85f4ff6
to
01ae66b
Compare
First constructions done; the itneresting ones will require being awake -:-)
…lds. s.f cannot be renamed to map...
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] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd suggest that you use EuclideanSpace ℝ n
and get rid of E
and H
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
/-- `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] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is not a class, right? How does Lean even accept it?
[dimension : finrank ℝ E = n] | |
dimension : finrank ℝ E = n |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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)
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
)?
## 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`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
`(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`. |
/-- 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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe call it I
instead of model
, to follow the convention in the rest of the library?
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a little bit strange to assume that phi is smooth, while continuous would do here, no?
|
||
/-- 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)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
noncomputable def comap [h: Fact (finrank ℝ E = n)] | |
noncomputable def comap [h : Fact (finrank ℝ E = n)] |
Same thing below
f := fun _ ↦ PUnit.unit | ||
hf := continuous_const | ||
|
||
/-- The product of a singular `n`- and a `m`-manifold into a one-point space |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
/-- 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 |
|
||
/-- 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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
-- FUTURE: prove that this observation inducess a commutative ring structure | |
-- FUTURE: prove that this observation induces a commutative ring structure |
These are used to define bordism groups: the
n
-bordism group of a topological spaceX
is the space of cobordism classes of all singularn
-manifolds onX
.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.