Documentation

TauCeti.Geometry.Manifold.Boundary.Model

The boundary model of a Euclidean half-space #

This file identifies the frontier of Mathlib's (n + 1)-dimensional manifold-with-boundary model ๐“กโˆ‚ (n + 1) with the boundaryless model ๐“ก n. Concretely, the frontier is the coordinate hyperplane where the zeroth coordinate vanishes; deleting that coordinate gives a continuous linear equivalence with EuclideanSpace โ„ (Fin n).

The construction is the standard-model prerequisite for putting a manifold structure on the boundary of a manifold modeled on a Euclidean half-space, as prescribed by Layer 1 of the GeometricTopology roadmap. The parametrization and projection API below is intended to let boundary charts use this identification without unfolding its coordinate construction. The file also splits the ambient Euclidean space into boundary and normal coordinates; the boundary inclusion and the standard product collar both use this one coordinate equivalence.

source
noncomputable def TauCeti.euclideanHalfSpaceBoundaryNormalEquiv (n : โ„•) :
(EuclideanSpace โ„ (Fin n) ร— โ„) โ‰ƒL[โ„] EuclideanSpace โ„ (Fin (n + 1))

Identify EuclideanSpace โ„ (Fin n) ร— โ„ with EuclideanSpace โ„ (Fin (n + 1)) by placing the real factor in the zeroth coordinate. The first factor parametrizes the boundary hyperplane and the second is its normal coordinate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.euclideanHalfSpaceBoundaryNormalEquiv_apply_zero (n : โ„•) (x : EuclideanSpace โ„ (Fin n)) (r : โ„) :
    ((euclideanHalfSpaceBoundaryNormalEquiv n) (x, r)).ofLp 0 = r

    The boundary-normal equivalence places the normal coordinate in coordinate zero.

    source
    @[simp]
    theorem TauCeti.euclideanHalfSpaceBoundaryNormalEquiv_apply_succ (n : โ„•) (x : EuclideanSpace โ„ (Fin n)) (r : โ„) (i : Fin n) :
    ((euclideanHalfSpaceBoundaryNormalEquiv n) (x, r)).ofLp i.succ = x.ofLp i

    The boundary-normal equivalence places the boundary coordinates after coordinate zero.

    source
    def TauCeti.euclideanHalfSpaceBoundary (n : โ„•) :
    Submodule โ„ (EuclideanSpace โ„ (Fin (n + 1)))

    The coordinate hyperplane which is the boundary of the (n + 1)-dimensional Euclidean half-space.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.mem_euclideanHalfSpaceBoundary {n : โ„•} {x : EuclideanSpace โ„ (Fin (n + 1))} :
      x โˆˆ euclideanHalfSpaceBoundary n โ†” x.ofLp 0 = 0
      source
      noncomputable def TauCeti.euclideanHalfSpaceBoundaryParam (n : โ„•) :
      EuclideanSpace โ„ (Fin n) โ†’L[โ„] EuclideanSpace โ„ (Fin (n + 1))

      Insert a zero as the zeroth coordinate, parametrizing the boundary of a Euclidean half-space by a Euclidean space of dimension one less.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.euclideanHalfSpaceBoundaryParam_apply_zero {n : โ„•} (x : EuclideanSpace โ„ (Fin n)) :
        ((euclideanHalfSpaceBoundaryParam n) x).ofLp 0 = 0
        source
        @[simp]
        theorem TauCeti.euclideanHalfSpaceBoundaryParam_apply_succ {n : โ„•} (x : EuclideanSpace โ„ (Fin n)) (i : Fin n) :
        ((euclideanHalfSpaceBoundaryParam n) x).ofLp i.succ = x.ofLp i
        source
        @[simp]
        theorem TauCeti.euclideanHalfSpaceBoundaryNormalEquiv_apply_zero_eq_boundaryParam (n : โ„•) (x : EuclideanSpace โ„ (Fin n)) :
        (euclideanHalfSpaceBoundaryNormalEquiv n) (x, 0) = (euclideanHalfSpaceBoundaryParam n) x

        The boundary-normal equivalence at normal coordinate zero is the boundary parametrization.

        source
        noncomputable def TauCeti.euclideanHalfSpaceBoundaryProj (n : โ„•) :
        EuclideanSpace โ„ (Fin (n + 1)) โ†’L[โ„] EuclideanSpace โ„ (Fin n)

        Delete the zeroth coordinate of a point in (n + 1)-dimensional Euclidean space.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.euclideanHalfSpaceBoundaryProj_apply {n : โ„•} (x : EuclideanSpace โ„ (Fin (n + 1))) (i : Fin n) :
          ((euclideanHalfSpaceBoundaryProj n) x).ofLp i = x.ofLp i.succ
          source
          @[simp]
          theorem TauCeti.euclideanHalfSpaceBoundaryNormalEquiv_symm_apply_fst (n : โ„•) (y : EuclideanSpace โ„ (Fin (n + 1))) :
          ((euclideanHalfSpaceBoundaryNormalEquiv n).symm y).1 = (euclideanHalfSpaceBoundaryProj n) y

          The boundary component of the inverse boundary-normal equivalence deletes coordinate zero.

          source
          @[simp]
          theorem TauCeti.euclideanHalfSpaceBoundaryNormalEquiv_symm_apply_snd (n : โ„•) (y : EuclideanSpace โ„ (Fin (n + 1))) :
          ((euclideanHalfSpaceBoundaryNormalEquiv n).symm y).2 = y.ofLp 0

          The normal component of the inverse boundary-normal equivalence is coordinate zero.

          source
          @[simp]
          theorem TauCeti.euclideanHalfSpaceBoundaryProj_param {n : โ„•} (x : EuclideanSpace โ„ (Fin n)) :
          (euclideanHalfSpaceBoundaryProj n) ((euclideanHalfSpaceBoundaryParam n) x) = x
          source
          @[simp]
          theorem TauCeti.euclideanHalfSpaceBoundaryParam_proj {n : โ„•} {x : EuclideanSpace โ„ (Fin (n + 1))} (hx : x โˆˆ euclideanHalfSpaceBoundary n) :
          (euclideanHalfSpaceBoundaryParam n) ((euclideanHalfSpaceBoundaryProj n) x) = x
          source
          @[simp]
          theorem TauCeti.euclideanHalfSpaceBoundaryParam_proj_eq_iff {n : โ„•} {x : EuclideanSpace โ„ (Fin (n + 1))} :
          (euclideanHalfSpaceBoundaryParam n) ((euclideanHalfSpaceBoundaryProj n) x) = x โ†” x โˆˆ euclideanHalfSpaceBoundary n
          source
          theorem TauCeti.euclideanHalfSpaceBoundaryParam_injective (n : โ„•) :
          Function.Injective โ‡‘(euclideanHalfSpaceBoundaryParam n)
          source
          @[simp]
          theorem TauCeti.range_euclideanHalfSpaceBoundaryParam (n : โ„•) :
          Set.range โ‡‘(euclideanHalfSpaceBoundaryParam n) = โ†‘(euclideanHalfSpaceBoundary n)
          source
          theorem TauCeti.euclideanHalfSpaceBoundary_eq_frontier (n : โ„•) :
          โ†‘(euclideanHalfSpaceBoundary n) = frontier (Set.range โ†‘(modelWithCornersEuclideanHalfSpace (n + 1)))

          The coordinate hyperplane is the frontier of Mathlib's Euclidean half-space model.

          source
          noncomputable def TauCeti.EuclideanHalfSpace.boundaryParam (n : โ„•) :
          EuclideanSpace โ„ (Fin n) โ†’ EuclideanHalfSpace (n + 1)

          Parametrize the boundary of the (n + 1)-dimensional Euclidean half-space by inserting a zero as the zeroth coordinate.

          Equations
          Instances For
            source
            noncomputable def TauCeti.EuclideanHalfSpace.boundaryProj (n : โ„•) :
            EuclideanHalfSpace (n + 1) โ†’ EuclideanSpace โ„ (Fin n)

            Delete the zeroth coordinate of a point of the (n + 1)-dimensional Euclidean half-space.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.EuclideanHalfSpace.boundaryParam_coe {n : โ„•} (x : EuclideanSpace โ„ (Fin n)) :
              โ†‘(boundaryParam n x) = (euclideanHalfSpaceBoundaryParam n) x

              The parametrized boundary point, read in the ambient Euclidean space.

              source
              @[simp]
              theorem TauCeti.EuclideanHalfSpace.boundaryProj_coe {n : โ„•} (y : EuclideanHalfSpace (n + 1)) :
              boundaryProj n y = (euclideanHalfSpaceBoundaryProj n) โ†‘y

              The boundary projection agrees with the ambient linear projection.

              source
              theorem TauCeti.EuclideanHalfSpace.boundaryProj_apply {n : โ„•} (y : EuclideanHalfSpace (n + 1)) (i : Fin n) :
              (boundaryProj n y).ofLp i = (โ†‘y).ofLp i.succ

              The coordinates of the boundary projection are the positive-index coordinates.

              source
              theorem TauCeti.EuclideanHalfSpace.boundaryProj_boundaryParam {n : โ„•} (x : EuclideanSpace โ„ (Fin n)) :
              boundaryProj n (boundaryParam n x) = x

              Deleting the zeroth coordinate undoes the boundary parametrization.

              source
              @[simp]
              theorem TauCeti.EuclideanHalfSpace.boundaryParam_boundaryProj {n : โ„•} {y : EuclideanHalfSpace (n + 1)} (hy : (โ†‘y).ofLp 0 = 0) :
              boundaryParam n ((euclideanHalfSpaceBoundaryProj n) โ†‘y) = y

              On the boundary of the half-space, deleting and reinserting the zeroth coordinate is the identity.

              source
              theorem TauCeti.EuclideanHalfSpace.continuous_boundaryParam {n : โ„•} :
              Continuous (boundaryParam n)

              The boundary parametrization is continuous.

              source
              theorem TauCeti.EuclideanHalfSpace.continuous_boundaryProj {n : โ„•} :
              Continuous (boundaryProj n)

              The boundary projection is continuous.

              source
              @[simp]
              theorem TauCeti.EuclideanHalfSpace.modelWithCornersEuclideanHalfSpace_symm_boundaryParam {n : โ„•} (x : EuclideanSpace โ„ (Fin n)) :
              โ†‘(modelWithCornersEuclideanHalfSpace (n + 1)).symm ((euclideanHalfSpaceBoundaryParam n) x) = boundaryParam n x

              The inverse of the model map ๐“กโˆ‚ (n + 1) sends the parametrized coordinate hyperplane to the boundary parametrization.

              source
              theorem TauCeti.EuclideanHalfSpace.boundaryParam_mem_range {n : โ„•} (x : EuclideanSpace โ„ (Fin n)) :
              (euclideanHalfSpaceBoundaryParam n) x โˆˆ Set.range โ†‘(modelWithCornersEuclideanHalfSpace (n + 1))

              The coordinate hyperplane lies in the range of the half-space model.

              source
              @[simp]
              theorem TauCeti.boundary_euclideanHalfSpace (n : โ„•) :
              ModelWithCorners.boundary (EuclideanHalfSpace (n + 1)) = {y : EuclideanHalfSpace (n + 1) | (โ†‘y).ofLp 0 = 0}

              The boundary of the Euclidean half-space, viewed as a manifold over itself, is the coordinate hyperplane where the zeroth coordinate vanishes.