Pulling back homological orientations along open embeddings

An open embedding j : M → N into a Hausdorff space identifies the integral local homology H_d(M, M ∖ {x}; ℤ) with H_d(N, N ∖ {j x}; ℤ) by excision (TauCeti.localHomologyIsoOfIsOpenEmbedding), and so identifies the local orientations at x with those at j x (Topology.IsOpenEmbedding.localOrientationEquiv). These identifications intertwine the transport of local orientations along paths (TauCeti.localHomologyTransport_comp_localHomologyIsoOfIsOpenEmbedding_hom). So an orientation o of N pulls back to an orientation o.comap hj of M, whose local orientation at x corresponds to the local orientation of o at j x (TauCeti.HomologicalOrientation.comap).

For the inclusion of an open subset this is the restriction of an orientation to the subset; in particular open subsets of orientable manifolds are orientable. For a homeomorphism e : M ≃ₜ N it compares orientations of M and of N: e is orientation-preserving for orientations o of M and o' of N when o'.comap e.isOpenEmbedding = o. In the dimension of a connected manifold M the pulled-back orientation is o or -o (TauCeti.HomologicalOrientation.eq_or_eq_neg), so such a homeomorphism either preserves or reverses orientation.

Main definitions

• Topology.IsOpenEmbedding.localOrientationEquiv: the local orientations of M at x and of N at j x correspond.
• TauCeti.HomologicalOrientation.comap: the pullback of an orientation along an open embedding.

Main results

• Topology.IsOpenEmbedding.localOrientationEquiv_id, Topology.IsOpenEmbedding.localOrientationEquiv_trans: the correspondence of local orientations is functorial.
• Topology.IsOpenEmbedding.localHomologyMap_localOrientationEquiv_symm: the map of local homology induced by j carries the local orientation corresponding to z back to z.
• IsOpen.localHomologyMap_inclusion_localOrientationEquiv_symm: the inclusion of open sets V ⊆ U carries the local orientations of V to the corresponding ones of U.
• TauCeti.HomologicalOrientation.localOrientationEquiv_comap_apply: the local orientation of the pullback at x corresponds to the local orientation at j x.
• TauCeti.HomologicalOrientation.comap_neg, TauCeti.HomologicalOrientation.comap_id, TauCeti.HomologicalOrientation.comap_comap: pullback commutes with reversal and is functorial.
• TauCeti.HomologicalOrientation.comap_symm_comap: pulling back along a homeomorphism and then along its inverse is the identity.

References

• A. Hatcher, Algebraic Topology, Section 3.3: local orientations, computed by excision in a neighbourhood, and orientations as locally consistent choices of local orientations.

noncomputable def Topology.IsOpenEmbedding.localOrientationEquiv {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : IsOpenEmbedding j) (x : M) (d : ℕ) : TauCeti.LocalOrientation M x d ≃ TauCeti.LocalOrientation N (j x) d

An open embedding j : M → N into a T₁ space identifies the local orientations of M at x in degree d with those of N at j x, through the isomorphism of integral local homology induced by j.

@[simp]

theorem Topology.IsOpenEmbedding.coe_localOrientationEquiv {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : IsOpenEmbedding j) (x : M) {d : ℕ} (z : TauCeti.LocalOrientation M x d) : ↑((hj.localOrientationEquiv x d) z) = (CategoryTheory.ConcreteCategory.hom (TauCeti.localHomologyIsoOfIsOpenEmbedding (↧(ULift.{w, 0} ℤ)) hj x d).hom) ↑z

On local homology classes, the correspondence of local orientations is the map induced by j.

@[simp]

theorem Topology.IsOpenEmbedding.coe_localOrientationEquiv_symm {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : IsOpenEmbedding j) (x : M) {d : ℕ} (z : TauCeti.LocalOrientation N (j x) d) : ↑((hj.localOrientationEquiv x d).symm z) = (CategoryTheory.ConcreteCategory.hom (TauCeti.localHomologyIsoOfIsOpenEmbedding (↧(ULift.{w, 0} ℤ)) hj x d).inv) ↑z

The inverse correspondence acts on local homology classes by the inverse isomorphism.

theorem Topology.IsOpenEmbedding.localHomologyMap_localOrientationEquiv_symm {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : IsOpenEmbedding j) (x : M) {d : ℕ} (z : TauCeti.LocalOrientation N (j x) d) (h : j ⁻¹' {j x} ⊆ {x}) : (CategoryTheory.ConcreteCategory.hom (TauCeti.localHomologyMap ↧(ULift.{w, 0} ℤ) { toFun := j, continuous_toFun := ⋯ } h d)) ↑((hj.localOrientationEquiv x d).symm z) = ↑z

The map of local homology induced by j carries the local orientation at x corresponding to a local orientation z at j x back to z.

@[simp]

theorem Topology.IsOpenEmbedding.localOrientationEquiv_neg {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : IsOpenEmbedding j) (x : M) {d : ℕ} (z : TauCeti.LocalOrientation M x d) : (hj.localOrientationEquiv x d) (-z) = -(hj.localOrientationEquiv x d) z

The correspondence of local orientations commutes with reversal.

@[simp]

theorem Topology.IsOpenEmbedding.localOrientationEquiv_id {M : Type w} [TopologicalSpace M] [T1Space M] (x : M) (d : ℕ) : ⋯.localOrientationEquiv x d = Equiv.refl (TauCeti.LocalOrientation M x d)

The identity identifies the local orientations at x with themselves.

@[simp]

theorem Topology.IsOpenEmbedding.localOrientationEquiv_trans {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} {P : Type w} [TopologicalSpace P] [T1Space P] {j' : N → P} (hj : IsOpenEmbedding j) (hj' : IsOpenEmbedding j') (x : M) (d : ℕ) : (hj.localOrientationEquiv x d).trans (hj'.localOrientationEquiv (j x) d) = ⋯.localOrientationEquiv x d

The correspondences of local orientations along open embeddings are functorial.

theorem IsOpen.localHomologyMap_inclusion_localOrientationEquiv_symm {N : Type w} [TopologicalSpace N] [T1Space N] {U V : Set N} (hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) {x : N} (hx : x ∈ V) {d : ℕ} (z : TauCeti.LocalOrientation N x d) (h : ⇑(ContinuousMap.inclusion hVU) ⁻¹' {⟨x, ⋯⟩} ⊆ {⟨x, hx⟩}) : (CategoryTheory.ConcreteCategory.hom (TauCeti.localHomologyMap (↧(ULift.{w, 0} ℤ)) (ContinuousMap.inclusion hVU) h d)) ↑((⋯.localOrientationEquiv ⟨x, hx⟩ d).symm z) = ↑((⋯.localOrientationEquiv ⟨x, ⋯⟩ d).symm z)

The inclusion of open sets V ⊆ U carries the local orientation of V at x corresponding to a local orientation z of the ambient space at x to the local orientation of U at x corresponding to z.

noncomputable def TauCeti.HomologicalOrientation.comap {M N E : Type w} [TopologicalSpace M] [T2Space M] [TopologicalSpace N] [T2Space N] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [ChartedSpace E N] {d : ℕ} {j : M → N} (o : HomologicalOrientation N E d) (hj : Topology.IsOpenEmbedding j) : HomologicalOrientation M E d

The pullback of an orientation along an open embedding j : M → N: the local orientation at x is the one corresponding to the local orientation of o at j x under the excision isomorphism induced by j.

theorem TauCeti.HomologicalOrientation.comap_apply {M N E : Type w} [TopologicalSpace M] [T2Space M] [TopologicalSpace N] [T2Space N] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [ChartedSpace E N] {d : ℕ} {j : M → N} (o : HomologicalOrientation N E d) (hj : Topology.IsOpenEmbedding j) (x : M) : (o.comap hj) x = (hj.localOrientationEquiv x d).symm (o (j x))

@[simp]

theorem TauCeti.HomologicalOrientation.localOrientationEquiv_comap_apply {M N E : Type w} [TopologicalSpace M] [T2Space M] [TopologicalSpace N] [T2Space N] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [ChartedSpace E N] {d : ℕ} {j : M → N} (o : HomologicalOrientation N E d) (hj : Topology.IsOpenEmbedding j) (x : M) : (hj.localOrientationEquiv x d) ((o.comap hj) x) = o (j x)

The local orientation of the pullback at x corresponds to the local orientation of o at j x.

theorem TauCeti.HomologicalOrientation.comap_congr {M N E : Type w} [TopologicalSpace M] [T2Space M] [TopologicalSpace N] [T2Space N] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [ChartedSpace E N] {d : ℕ} {j : M → N} (o : HomologicalOrientation N E d) {j' : M → N} (hj : Topology.IsOpenEmbedding j) (hj' : Topology.IsOpenEmbedding j') (hjj' : j = j') : o.comap hj = o.comap hj'

The pullback depends only on the open embedding as a function, not on the proof that it is one.

@[simp]

theorem TauCeti.HomologicalOrientation.comap_neg {M N E : Type w} [TopologicalSpace M] [T2Space M] [TopologicalSpace N] [T2Space N] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [ChartedSpace E N] {d : ℕ} {j : M → N} (o : HomologicalOrientation N E d) (hj : Topology.IsOpenEmbedding j) : (-o).comap hj = -o.comap hj

Pulling back commutes with reversing orientations.

@[simp]

theorem TauCeti.HomologicalOrientation.comap_id {M E : Type w} [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] {d : ℕ} (o : HomologicalOrientation M E d) : o.comap ⋯ = o

Pulling back along the identity does not change an orientation.

theorem TauCeti.HomologicalOrientation.comap_comap {M N P E : Type w} [TopologicalSpace M] [T2Space M] [TopologicalSpace N] [T2Space N] [TopologicalSpace P] [T2Space P] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [ChartedSpace E N] [ChartedSpace E P] {d : ℕ} {j : M → N} (o : HomologicalOrientation P E d) {j' : N → P} (hj' : Topology.IsOpenEmbedding j') (hj : Topology.IsOpenEmbedding j) : (o.comap hj').comap hj = o.comap ⋯

Pulling back is functorial: pulling back along j an orientation pulled back along j' is pulling back along j' ∘ j.

@[simp]

theorem TauCeti.HomologicalOrientation.comap_symm_comap {M N E : Type w} [TopologicalSpace M] [T2Space M] [TopologicalSpace N] [T2Space N] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [ChartedSpace E N] {d : ℕ} (o : HomologicalOrientation N E d) (e : M ≃ₜ N) : (o.comap ⋯).comap ⋯ = o

Pulling an orientation back along a homeomorphism and then along its inverse gives it back.