OAI/Geometry/EinsteinFour/OrientationCoverCharts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Smooth local coordinates on the actual orientation cover. The projection identifies each sheet with a base chart.

  1. def OAI.PositiveEinsteinFour.Geometry.orientationCoverLocal line 18
  2. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverLocal_apply line 21
  3. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverLocal_mem line 25
  4. def OAI.PositiveEinsteinFour.Geometry.orientationCoverChart line 29
  5. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverChart_apply line 33
  6. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverChart_mem line 38
  7. theorem OAI.PositiveEinsteinFour.Geometry.orientationCoverChart_inverse_proj line 42
  8. instance OAI.PositiveEinsteinFour.Geometry.orientationCover_chartedSpace line 49
  9. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_transition_eq line 56

    Source documentation

    Each change of sheets uses precisely the base chart transition.

    theorem orientationCover_transition_eq (x y : OrientationCover M) {z : FourSpace}
    (hz : z ∈ ((orientationCoverChart x).symm.trans (orientationCoverChart y)).source) :
    ((orientationCoverChart x).symm.trans (orientationCoverChart y)) z =
      chartAt FourSpace y.proj ((chartAt FourSpace x.proj).symm z) := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.OrientationCover, OAI.PositiveEinsteinFour.Geometry.orientationCoverChart

  10. theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_transition_source line 63
  11. instance OAI.PositiveEinsteinFour.Geometry.orientationCover_isManifold line 73