OrientationCoverCore.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The actual orientation double cover, obtained by applying the determinant sign representation to the tangent bundle's transition functions. Its two-point fibers are glued by the genuine derivatives of chart changes.

abbrev OAI.PositiveEinsteinFour.Geometry.TC line 21
abbrev OAI.PositiveEinsteinFour.Geometry.CI line 22
def OAI.PositiveEinsteinFour.Geometry.orientationTransitionDet line 25
Source documentation
Determinant of the actual tangent transition, from chart i to chart j.
```
def orientationTransitionDet (i j : CI (M := M)) (x : M) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CI
theorem OAI.PositiveEinsteinFour.Geometry.orientationTransitionDet_self line 28
theorem OAI.PositiveEinsteinFour.Geometry.orientationTransitionDet_comp line 38
theorem OAI.PositiveEinsteinFour.Geometry.orientationTransitionDet_ne_zero line 47
theorem OAI.PositiveEinsteinFour.Geometry.orientationTransitionDet_continuousOn line 55
def OAI.PositiveEinsteinFour.Geometry.orientationSignChange line 59
theorem OAI.PositiveEinsteinFour.Geometry.orientationSignChange_mul line 61
theorem OAI.PositiveEinsteinFour.Geometry.orientationTransition_continuousOn line 76
def OAI.PositiveEinsteinFour.Geometry.orientationCoverCore line 98
Source documentation
The orientation cover is a bundle with the determinant-sign cocycle.
```
def orientationCoverCore : FiberBundleCore (CI (M := M)) M Bool where
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CI
abbrev OAI.PositiveEinsteinFour.Geometry.OrientationCover line 113
theorem OAI.PositiveEinsteinFour.Geometry.orientationCover_isCoveringMap line 117
Source documentation
The projection has exactly two sheets, with actual bundle trivializations.
```
theorem orientationCover_isCoveringMap :
    IsCoveringMap (orientationCoverCore (M := M)).proj := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.orientationCoverCore