Theorems · Inductive type · manifolds

SingularManifold

(X : Type u_1) →
  [TopologicalSpace X] →
    WithTop ℕ∞ →
      {E : Type u_2} →
        {H : Type u_3} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [FiniteDimensional ℝ E] →
                [inst_3 : TopologicalSpace H] → ModelWithCorners ℝ E H → Type (max (max (u + 1) u_1) u_3)

A singular manifold on a topological space X is a pair (M, f) of a closed C^k-manifold M modelled on I together with a continuous map M → X. If we wish to emphasize the model, we will speak of a singular I-manifold. In practice, one commonly wants to take k=∞ (as then e.g. the intersection form is a powerful tool to compute bordism groups; for the definition, this makes no difference.) This is parametrised on the universe M lives in; ensure u is the first universe argument.

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

14 results in Mathlib

Foundations

Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpace