Documentation

Atlas.GeometryOfManifolds.code.TrivialDFS

source
@[reducible]
def TrivialΩ :
ℕ → Type u_1

Trivial differential-form scaffolding: every degree's space of forms is the singleton PUnit, providing a degenerate witness for the DFS API.

Instances For
    source
    @[reducible]
    def TrivialVF :
    Type u_1

    Trivial vector-field space: the singleton PUnit, the partner of TrivialΩ.

    Instances For
      source
      @[implicit_reducible]
      noncomputable instance trivialDFS :
      DifferentialFormSpace TrivialΩ TrivialVF

      The trivial DifferentialFormSpace instance on TrivialΩ / TrivialVF: all operations return the unique element of PUnit and all axioms hold by Subsingleton.elim.