Documentation

TauCeti.Geometry.Manifold.Orientation.Basic

Orientations of manifolds with corners #

A manifold orientation is a source-indexed orientation lift modulo simultaneous reversal of its model orientation and all chart signs. It induces an actual, locally constant orientation of the tangent bundle. This definition includes boundary and corner points. Orientability records existence; every model with corners is orientable.

Reindexing along an equivalence of index types (TauCeti.Manifold.Orientation.reindex) reindexes every tangent orientation. It compares orientations indexed by Fin (m + n) and Fin (n + m), such as the products of two oriented manifolds taken in either order.

Orientability records existence; every model with corners is orientable, and TauCeti.Manifold.Orientation.congrModel casts manifold orientations along an equality of models.

source
def TauCeti.Manifold.Orientation {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [FiniteDimensional ℝ E] (M : Type u_5) [TopologicalSpace M] [ChartedSpace H M] (ι : Type u_6) [Fintype ι] :
Type (max (max u_1 u_5) u_6)

An orientation of a manifold, including its boundary and corners.

Instances For
    source
    def TauCeti.Manifold.Orientation.mk {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : OrientationLift I M ι) :
    Orientation I M ι

    The orientation represented by a lift.

    Instances For
      source
      theorem TauCeti.Manifold.Orientation.mk_eq_mk_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (a b : OrientationLift I M ι) :
      mk a = mk b ↔ a = b ∨ a = b.flip

      Two lifts represent the same orientation exactly when they agree or differ by the simultaneous reversal of model orientation and source signs.

      source
      def TauCeti.Manifold.Orientation.lift {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {α : Sort u_5} (f : OrientationLift I M ι → α) (hflip : ∀ (l : OrientationLift I M ι), f l.flip = f l) :
      Orientation I M ι → α

      Define a function on orientations from a function on lifts invariant under diagonal flip.

      Instances For
        source
        @[simp]
        theorem TauCeti.Manifold.Orientation.lift_mk {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {α : Sort u_5} (f : OrientationLift I M ι → α) (hflip : ∀ (l : OrientationLift I M ι), f l.flip = f l) (l : OrientationLift I M ι) :
        lift f hflip (mk l) = f l

        A function induced from lifts evaluates on a represented orientation at its lift.

        source
        theorem TauCeti.Manifold.Orientation.exists_lift {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) :
        ∃ (l : OrientationLift I M ι), mk l = o

        Every manifold orientation has a source-indexed lift.

        source
        theorem TauCeti.Manifold.Orientation.exists_lift_modelOrientation_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) (m : _root_.Orientation ℝ E ι) :
        ∃ (l : OrientationLift I M ι), mk l = o ∧ l.modelOrientation = m

        Every manifold orientation has a lift with any prescribed model orientation, obtained by flipping an arbitrary lift if necessary.

        source
        theorem TauCeti.Manifold.Orientation.inductionOn {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {p : Orientation I M ι → Prop} (o : Orientation I M ι) (h : ∀ (l : OrientationLift I M ι), p (mk l)) :
        p o

        Prove a property of orientations by proving it for every source-indexed lift.

        source
        theorem TauCeti.Manifold.Orientation.card_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) :
        Fintype.card ι = Module.finrank ℝ E

        The index type has the dimension of the model space.

        source
        theorem TauCeti.Manifold.Orientation.finrank_tangentSpace_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) (x : M) :
        Module.finrank ℝ (TangentSpace I x) = Fintype.card ι

        The tangent space has the dimension encoded by the orientation index.

        source
        theorem TauCeti.Manifold.Orientation.fact_finrank_tangentSpace {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {m : ℕ} (o : Orientation I M (Fin m)) (x : M) :
        Fact (Module.finrank ℝ (TangentSpace I x) = m)

        The orientation index supplies the tangent-space finrank as a Fact instance.

        source
        def TauCeti.Manifold.Orientation.neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) :
        Orientation I M ι

        Reverse the tangent orientations by reversing the model orientation of a lift.

        Instances For
          source
          @[instance_reducible]
          instance TauCeti.Manifold.Orientation.instNeg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] :
          Neg (Orientation I M ι)
          source
          @[simp]
          theorem TauCeti.Manifold.Orientation.neg_mk {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : OrientationLift I M ι) :
          -mk o = mk (-o)
          source
          def TauCeti.Manifold.Orientation.reindex {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {ι' : Type u_5} [Fintype ι'] (e : ι ≃ ι') (o : Orientation I M ι) :
          Orientation I M ι'

          Reindex a manifold orientation along an equivalence of index types.

          Instances For
            source
            @[simp]
            theorem TauCeti.Manifold.Orientation.reindex_mk {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {ι' : Type u_5} [Fintype ι'] (e : ι ≃ ι') (o : OrientationLift I M ι) :
            reindex e (mk o) = mk (OrientationLift.reindex e o)
            source
            noncomputable def TauCeti.Manifold.Orientation.toVectorBundleOrientation {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (o : Orientation I M ι) :
            VectorBundleOrientation E (TangentSpace I) ι

            The induced orientation of the tangent bundle.

            Instances For
              source
              @[simp]
              theorem TauCeti.Manifold.Orientation.toVectorBundleOrientation_mk {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (o : OrientationLift I M ι) :
              (mk o).toVectorBundleOrientation = o.toVectorBundleOrientation
              source
              @[simp]
              theorem TauCeti.Manifold.Orientation.toVectorBundleOrientation_neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (o : Orientation I M ι) :
              (-o).toVectorBundleOrientation = -o.toVectorBundleOrientation
              source
              noncomputable def TauCeti.Manifold.Orientation.orientationAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (o : Orientation I M ι) (x : M) :
              _root_.Orientation ℝ (TangentSpace I x) ι

              The orientation of a tangent space induced by a manifold orientation.

              Instances For
                source
                @[simp]
                theorem TauCeti.Manifold.Orientation.toVectorBundleOrientation_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (o : Orientation I M ι) (x : M) :
                o.toVectorBundleOrientation x = o.orientationAt x

                Evaluation of the tangent-bundle interpretation is the manifold's tangent orientation.

                source
                @[simp]
                theorem TauCeti.Manifold.Orientation.orientationAt_mk {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (o : OrientationLift I M ι) (x : M) :
                (mk o).orientationAt x = o.orientationAt x

                The tangent orientation of a represented manifold orientation is the representative's intrinsic tangent orientation, including at boundary and corner points.

                source
                @[simp]
                theorem TauCeti.Manifold.Orientation.orientationAt_neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (o : Orientation I M ι) (x : M) :
                (-o).orientationAt x = -o.orientationAt x
                source
                @[simp]
                theorem TauCeti.Manifold.Orientation.orientationAt_reindex {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] {ι' : Type u_5} [Fintype ι'] (e : ι ≃ ι') (o : Orientation I M ι) (x : M) :
                (reindex e o).orientationAt x = (_root_.Orientation.reindex ℝ (TangentSpace I x) e) (o.orientationAt x)

                Reindexing a manifold orientation reindexes each of its tangent orientations.

                source
                theorem TauCeti.Manifold.Orientation.ext {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] {o o' : Orientation I M ι} (h : ∀ (x : M), o.orientationAt x = o'.orientationAt x) :
                o = o'

                A manifold orientation is determined by its actual tangent orientations.

                source
                theorem TauCeti.Manifold.Orientation.ext_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] {o o' : Orientation I M ι} :
                o = o' ↔ ∀ (x : M), o.orientationAt x = o'.orientationAt x
                source
                theorem TauCeti.Manifold.Orientation.eq_or_eq_neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] [PreconnectedSpace M] (o o' : Orientation I M ι) :
                o = o' ∨ o = -o'

                Over a preconnected manifold there are at most two orientations.

                source
                theorem TauCeti.Manifold.Orientation.neg_ne_self {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [Nonempty M] (o : Orientation I M ι) :
                -o ≠ o

                An orientation differs from its opposite on every nonempty manifold.

                source
                theorem TauCeti.Manifold.Orientation.neg_neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : Orientation I M ι) :
                - -o = o
                source
                @[instance_reducible]
                instance TauCeti.Manifold.Orientation.instInvolutiveNeg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] :
                InvolutiveNeg (Orientation I M ι)
                source
                @[simp]
                theorem TauCeti.Manifold.Orientation.reindex_neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {ι' : Type u_5} [Fintype ι'] (e : ι ≃ ι') (o : Orientation I M ι) :
                reindex e (-o) = -reindex e o
                source
                noncomputable def TauCeti.Manifold.Orientation.ofVectorBundleOrientation {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (model : _root_.Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) (o : VectorBundleOrientation E (TangentSpace I) ι) :
                Orientation I M ι

                Construct a manifold orientation from a locally constant orientation of its tangent bundle. The choice of model orientation affects only its representative lift.

                Instances For
                  source
                  @[simp]
                  theorem TauCeti.Manifold.Orientation.orientationAt_ofVectorBundleOrientation {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (model : _root_.Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) (o : VectorBundleOrientation E (TangentSpace I) ι) (x : M) :
                  (ofVectorBundleOrientation model hι o).orientationAt x = o x
                  source
                  @[simp]
                  theorem TauCeti.Manifold.Orientation.toVectorBundleOrientation_ofVectorBundleOrientation {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (model : _root_.Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) (o : VectorBundleOrientation E (TangentSpace I) ι) :
                  (ofVectorBundleOrientation model hι o).toVectorBundleOrientation = o

                  Interpreting the orientation reconstructed from tangent orientations recovers the bundle orientation.

                  source
                  @[simp]
                  theorem TauCeti.Manifold.Orientation.ofVectorBundleOrientation_toVectorBundleOrientation {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] [IsManifold I 1 M] (model : _root_.Orientation ℝ E ι) (o : Orientation I M ι) :
                  ofVectorBundleOrientation model ⋯ o.toVectorBundleOrientation = o

                  Recovering a manifold orientation from its tangent bundle orientations is independent of the chosen model orientation.

                  source
                  def TauCeti.Manifold.Orientation.model {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : _root_.Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) :
                  Orientation I H ι

                  The constant orientation of a model with corners.

                  Instances For
                    source
                    theorem TauCeti.Manifold.Orientation.model_eq_mk {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : _root_.Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) :
                    model o hι = mk (OrientationLift.ofHasGroupoid o hι)

                    The constant model orientation is represented by its actual constant orientation lift.

                    source
                    @[simp]
                    theorem TauCeti.Manifold.Orientation.orientationAt_model {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] (o : _root_.Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E) (x : H) :
                    (model o hι).orientationAt x = o
                    source
                    noncomputable def TauCeti.Manifold.Orientation.real :
                    Orientation (modelWithCornersSelf ℝ ℝ) ℝ (Fin 1)

                    The standard orientation of ℝ, in which the unit vector 1 is positive.

                    Instances For
                      source
                      theorem TauCeti.Manifold.Orientation.real_eq_model :
                      real = model (Module.Basis.singleton (Fin 1) ℝ).orientation real_eq_model._proof_1

                      The standard orientation of ℝ is the constant model orientation of the singleton basis.

                      source
                      @[simp]
                      theorem TauCeti.Manifold.Orientation.orientationAt_real (x : ℝ) :
                      real.orientationAt x = (Module.Basis.singleton (Fin 1) ℝ).orientation

                      At every point of ℝ, the standard orientation is the orientation of the singleton basis.

                      source
                      def TauCeti.Manifold.Orientation.congrModel {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {I J : ModelWithCorners ℝ E H} (h : I = J) (o : Orientation I M ι) :
                      Orientation J M ι

                      Cast a manifold orientation along an equality of models on the same model vector space and chart carrier.

                      Instances For
                        source
                        @[simp]
                        theorem TauCeti.Manifold.Orientation.congrModel_mk {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {I J : ModelWithCorners ℝ E H} (h : I = J) (l : OrientationLift I M ι) :
                        congrModel h (mk l) = mk (OrientationLift.congrModel h l)
                        source
                        @[simp]
                        theorem TauCeti.Manifold.Orientation.congrModel_refl {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {I : ModelWithCorners ℝ E H} (o : Orientation I M ι) :
                        congrModel ⋯ o = o
                        source
                        @[simp]
                        theorem TauCeti.Manifold.Orientation.congrModel_congrModel {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {I J K : ModelWithCorners ℝ E H} (h₁ : I = J) (h₂ : J = K) (o : Orientation I M ι) :
                        congrModel h₂ (congrModel h₁ o) = congrModel ⋯ o
                        source
                        @[simp]
                        theorem TauCeti.Manifold.Orientation.neg_congrModel {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {I J : ModelWithCorners ℝ E H} (h : I = J) (o : Orientation I M ι) :
                        congrModel h (-o) = -congrModel h o
                        source
                        theorem TauCeti.Manifold.Orientation.congrModel_injective {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {I J : ModelWithCorners ℝ E H} (h : I = J) :
                        Function.Injective (congrModel h)
                        source
                        @[simp]
                        theorem TauCeti.Manifold.Orientation.congrModel_inj {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {I J : ModelWithCorners ℝ E H} (h : I = J) {o₁ o₂ : Orientation I M ι} :
                        congrModel h o₁ = congrModel h o₂ ↔ o₁ = o₂
                        source
                        @[simp]
                        theorem TauCeti.Manifold.Orientation.orientationAt_congrModel {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] {ι : Type u_4} [Fintype ι] {I J : ModelWithCorners ℝ E H} (h : I = J) [IsManifold I 1 M] [IsManifold J 1 M] (o : Orientation I M ι) (x : M) :
                        (congrModel h o).orientationAt x = o.orientationAt x
                        source
                        class TauCeti.Orientable {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] :
                        Prop

                        A manifold with corners is orientable when it carries an orientation of its tangent spaces compatible with the within-range chart Jacobians.

                        Instances
                          source
                          instance TauCeti.instOrientable {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} :
                          Orientable I H

                          Every model with corners carries its constant model orientation.

                          source
                          theorem TauCeti.orientable_iff_nonempty_vectorBundleOrientation {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] :
                          Orientable I M ↔ Nonempty (VectorBundleOrientation E (TangentSpace I) (Fin (Module.finrank ℝ E)))

                          A manifold is orientable exactly when its tangent bundle is orientable.