Transport of local orientations

The integral local homology system transports generators along paths. This file restricts its transport to equivalences between the sets of local orientations, compatible with identities, composition, path reversal and orientation reversal. They act on the generator fibres of the existing integral local homology system.

The underlying local homology transport is described through compact convex sets in charts by TauCeti.localHomologyRestriction_comp_localHomologyTransport in TauCeti.AlgebraicTopology.Singular.LocalHomology.System.

The transport is defined in every degree; in the dimension of a manifold its fibres have two orientations, as described by TauCeti.isLocalOrientation_iff_eq_or_eq_neg_inv_one and the chart computation of local homology.

References

• A. Hatcher, Algebraic Topology, Section 3.3: transport of local orientations through local homology over balls.

noncomputable def TauCeti.localOrientationTransport (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (d : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) : LocalOrientation M x.as d ≃ LocalOrientation M y.as d

Transport of local orientations along a path class, obtained by restricting the integral local homology transport to its generators.

@[simp]

theorem TauCeti.coe_localOrientationTransport (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (d : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) (z : LocalOrientation M x.as d) : ↑((localOrientationTransport M E d f) z) = (CategoryTheory.ConcreteCategory.hom (localHomologyTransport (↧(ULift.{w, 0} ℤ)) M E d f)) ↑z

On local homology classes, orientation transport is the integral local homology transport.

@[simp]

theorem TauCeti.coe_localOrientationTransport_symm (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (d : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) (z : LocalOrientation M y.as d) : ↑((localOrientationTransport M E d f).symm z) = (CategoryTheory.ConcreteCategory.hom (localHomologyTransport (↧(ULift.{w, 0} ℤ)) M E d (CategoryTheory.inv f))) ↑z

The inverse equivalence acts on classes by transport along the reversed path.

@[simp]

theorem TauCeti.localOrientationTransport_id (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (d : ℕ) (x : FundamentalGroupoid M) : localOrientationTransport M E d (CategoryTheory.CategoryStruct.id x) = Equiv.refl (LocalOrientation M x.as d)

@[simp]

theorem TauCeti.localOrientationTransport_comp (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (d : ℕ) {x y z : FundamentalGroupoid M} (f : x ⟶ y) (g : y ⟶ z) : localOrientationTransport M E d (CategoryTheory.CategoryStruct.comp f g) = (localOrientationTransport M E d f).trans (localOrientationTransport M E d g)

Transport along a composite is successive transport along its two paths.

@[simp]

theorem TauCeti.localOrientationTransport_inv (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (d : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) : localOrientationTransport M E d (CategoryTheory.inv f) = (localOrientationTransport M E d f).symm

Reversing a path inverts its equivalence of local orientations.

@[simp]

theorem TauCeti.localOrientationTransport_neg (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (d : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) (z : LocalOrientation M x.as d) : (localOrientationTransport M E d f) (-z) = -(localOrientationTransport M E d f) z

Transport commutes with reversal of local orientations.