Local orientations from chart homology

A local orientation at a point of an n-dimensional manifold is a generator of the integral local homology group in degree n. This file defines that generator condition and proves that every point in a finite-dimensional charted space has local orientations. Integral coefficients are represented by the universe-lifted module ULift ℤ. The construction is the inverse image of 1 under the chart computation of local homology. The two generators of a fibre isomorphic to ℤ differ by sign; reversal and preservation by local homology isomorphisms are also proved, and isomorphisms of pairs (M, M ∖ {x}) ≅ (N, N ∖ {y}) transport local orientations (TauCeti.LocalOrientation.map), compatibly with reversal, identities and composites.

The local orientation is the generator of Hₙ(M, M ∖ {x}; ℤ) described in Hatcher's Algebraic Topology, Section 3.3.

def TauCeti.IsLocalOrientation {M : Type w} [TopologicalSpace M] (x : M) (d : ℕ) (z : ↑(localHomology ↧(ULift.{w, 0} ℤ) {x} d)) : Prop

An element of the integral local homology group is a local orientation when it generates the whole group as a ℤ-module.

theorem TauCeti.isLocalOrientation_iff {M : Type w} [TopologicalSpace M] (x : M) (d : ℕ) (z : ↑(localHomology ↧(ULift.{w, 0} ℤ) {x} d)) : IsLocalOrientation x d z ↔ ∀ (y : ↑(localHomology ↧(ULift.{w, 0} ℤ) {x} d)), ∃ (c : ℤ), c • z = y

An element of local homology is a local orientation exactly when every class is an integral multiple of it.

@[reducible, inline]

abbrev TauCeti.LocalOrientation (M : Type w) [TopologicalSpace M] (x : M) (d : ℕ) : Type w

The integral local homology group at x in degree d, with its local orientations.

theorem TauCeti.isLocalOrientation_inv_one {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} (e : localHomology ↧(ULift.{w, 0} ℤ) {x} d ≅ ↧(ULift.{w, 0} ℤ)) : IsLocalOrientation x d ((CategoryTheory.ConcreteCategory.hom e.inv) 1)

The inverse image of 1 under an isomorphism from integral local homology to ℤ is a local orientation.

theorem TauCeti.IsLocalOrientation.neg {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} {z : ↑(localHomology ↧(ULift.{w, 0} ℤ) {x} d)} (hz : IsLocalOrientation x d z) : IsLocalOrientation x d (-z)

Reversing a local orientation gives a local orientation.

@[instance_reducible]

noncomputable instance TauCeti.instInvolutiveNegLocalOrientation {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} : InvolutiveNeg (LocalOrientation M x d)

Reversal of local orientations is involutive.

@[simp]

theorem TauCeti.LocalOrientation.coe_neg {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} (z : LocalOrientation M x d) : ↑(-z) = -↑z

theorem TauCeti.IsLocalOrientation.map {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] {x : M} {y : N} {d : ℕ} {z : ↑(localHomology ↧(ULift.{w, 0} ℤ) {x} d)} (hz : IsLocalOrientation x d z) (e : localHomology ↧(ULift.{w, 0} ℤ) {x} d ≅ localHomology ↧(ULift.{w, 0} ℤ) {y} d) : IsLocalOrientation y d ((CategoryTheory.ConcreteCategory.hom e.hom) z)

An isomorphism of integral local homology groups preserves the generator condition.

noncomputable def TauCeti.LocalOrientation.map {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] {x : M} {y : N} {d : ℕ} (z : LocalOrientation M x d) (e : TopPair.ofSubset {x}ᶜ ≅ TopPair.ofSubset {y}ᶜ) : LocalOrientation N y d

An isomorphism of pairs (M, M ∖ {x}) ≅ (N, N ∖ {y}) carries local orientations at x to local orientations at y, through the isomorphism it induces on integral local homology.

@[simp]

theorem TauCeti.LocalOrientation.coe_map {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] {x : M} {y : N} {d : ℕ} (z : LocalOrientation M x d) (e : TopPair.ofSubset {x}ᶜ ≅ TopPair.ofSubset {y}ᶜ) : ↑(z.map e) = (ModuleCat.Hom.hom (TopPair.singularHomologyMap e.hom (↧(ULift.{w, 0} ℤ)) d)) ↑z

@[simp]

theorem TauCeti.LocalOrientation.map_neg {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] {x : M} {y : N} {d : ℕ} (z : LocalOrientation M x d) (e : TopPair.ofSubset {x}ᶜ ≅ TopPair.ofSubset {y}ᶜ) : (-z).map e = -z.map e

Transport along an isomorphism of pairs commutes with reversal of local orientations.

@[simp]

theorem TauCeti.LocalOrientation.map_refl {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} (z : LocalOrientation M x d) : z.map (CategoryTheory.Iso.refl (TopPair.ofSubset {x}ᶜ)) = z

Transport along the identity isomorphism of pairs is the identity.

theorem TauCeti.LocalOrientation.map_trans {M N P : Type w} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] {x : M} {y : N} {p : P} {d : ℕ} (z : LocalOrientation M x d) (e : TopPair.ofSubset {x}ᶜ ≅ TopPair.ofSubset {y}ᶜ) (e' : TopPair.ofSubset {y}ᶜ ≅ TopPair.ofSubset {p}ᶜ) : z.map (e ≪≫ e') = (z.map e).map e'

Transport along a composite isomorphism of pairs is the composite of the transports.

theorem TauCeti.isLocalOrientation_iff_eq_or_eq_neg_inv_one {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} (e : localHomology ↧(ULift.{w, 0} ℤ) {x} d ≅ ↧(ULift.{w, 0} ℤ)) (z : ↑(localHomology ↧(ULift.{w, 0} ℤ) {x} d)) : IsLocalOrientation x d z ↔ z = (CategoryTheory.ConcreteCategory.hom e.inv) 1 ∨ z = -(CategoryTheory.ConcreteCategory.hom e.inv) 1

If integral local homology is isomorphic to ℤ, its generators are precisely the inverse images of 1 and -1. In particular a top-degree local homology fibre has two orientations.

theorem TauCeti.nat_card_localOrientation {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} (e : localHomology ↧(ULift.{w, 0} ℤ) {x} d ≅ ↧(ULift.{w, 0} ℤ)) : Nat.card (LocalOrientation M x d) = 2

A local homology fibre isomorphic to ℤ has exactly two local orientations.

theorem TauCeti.IsLocalOrientation.eq_or_eq_neg {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} (e : localHomology ↧(ULift.{w, 0} ℤ) {x} d ≅ ↧(ULift.{w, 0} ℤ)) {z z' : ↑(localHomology ↧(ULift.{w, 0} ℤ) {x} d)} (hz : IsLocalOrientation x d z) (hz' : IsLocalOrientation x d z') : z' = z ∨ z' = -z

In a local homology fibre isomorphic to ℤ, two local orientations agree up to sign.

theorem TauCeti.IsLocalOrientation.zsmul_eq_zero_iff {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} (e : localHomology ↧(ULift.{w, 0} ℤ) {x} d ≅ ↧(ULift.{w, 0} ℤ)) {z : ↑(localHomology ↧(ULift.{w, 0} ℤ) {x} d)} (hz : IsLocalOrientation x d z) {c : ℤ} : c • z = 0 ↔ c = 0

In a local homology fibre isomorphic to ℤ, a local orientation has infinite order.

theorem TauCeti.IsLocalOrientation.neg_ne {M : Type w} [TopologicalSpace M] {x : M} {d : ℕ} (e : localHomology ↧(ULift.{w, 0} ℤ) {x} d ≅ ↧(ULift.{w, 0} ℤ)) {z : ↑(localHomology ↧(ULift.{w, 0} ℤ) {x} d)} (hz : IsLocalOrientation x d z) : -z ≠ z

In a local homology fibre isomorphic to ℤ, a local orientation differs from its reversal.

noncomputable def TauCeti.localOrientationOfChart {M E : Type w} [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] (φ : OpenPartialHomeomorph M E) {x : M} (hx : x ∈ φ.source) {n : ℕ} (hn : Module.finrank ℝ E = n + 1) : LocalOrientation M x (n + 1)

The local orientation at x selected by a chart and its chart-induced local homology isomorphism.

theorem TauCeti.exists_localOrientation_of_chart {M E : Type w} [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [ChartedSpace E M] (x : M) {n : ℕ} (hn : Module.finrank ℝ E = n + 1) : Nonempty (LocalOrientation M x (n + 1))

A point in a positive-dimensional finite-dimensional charted space has a local orientation. The chart computation identifies its local homology group with ℤ, and the inverse image of 1 is a generator.

noncomputable def TauCeti.localOrientationOfZeroDimChart {M E : Type w} [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (φ : OpenPartialHomeomorph M E) {x : M} (hx : x ∈ φ.source) (hn : Module.finrank ℝ E = 0) : LocalOrientation M x 0

A point with a zero-dimensional chart also has a local orientation, represented by the class of the point in degree-zero local homology.

theorem TauCeti.exists_localOrientation_of_zero_dim_chart {M E : Type w} [TopologicalSpace M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (x : M) (hn : Module.finrank ℝ E = 0) : Nonempty (LocalOrientation M x 0)

Every point of a zero-dimensional finite-dimensional charted space has a local orientation.