Bridge between Sphere n and TopCat.sphere n

The project uses the concrete metric-sphere subtype for antipodal actions and quotients, while Mathlib's algebraic-topology APIs use TopCat.sphere n. This module proves that the two models differ only by ULift, packages the resulting homeomorphism and categorical isomorphism, and transports continuous maps between the models with identity and composition laws.

theorem SphereOddDegree.topCatSphere_carrier_eq (n : ℕ) : ↑(TopCat.sphere n) = ULift.{u, 0} (Sphere n)

The carrier type of TopCat.sphere n is definitionally ULift (Sphere n): the ambient space and the metric-sphere subtype agree exactly, and the only difference is the universe-lifting ULift wrapper used by the TopCat object.

noncomputable def SphereOddDegree.topCatSphereHomeomorph (n : ℕ) : ↑(TopCat.sphere n) ≃ₜ Sphere n

TopCat.sphere n is homeomorphic to the raw subtype model Sphere n. The homeomorphism is simply the universe-lift equivalence Homeomorph.ulift, witnessing that the two models differ only by a ULift wrapper.

Equations

• SphereOddDegree.topCatSphereHomeomorph n = Homeomorph.ulift

noncomputable def SphereOddDegree.topCatSphereIso (n : ℕ) : TopCat.sphere n ≅ ↧(Sphere n)

TopCat.sphere n is isomorphic, as an object of TopCat, to the raw subtype model Sphere n packaged with TopCat.of. This is the categorical packaging of topCatSphereHomeomorph through TopCat.isoOfHomeo; like the homeomorphism it carries no mathematical content beyond the universe-lifting ULift wrapper.

Use this to transport TopCat-phrased algebraic-topology constructions (e.g. categorical (co)homology of TopCat.sphere n) onto the library's working model Sphere n.

Equations

• SphereOddDegree.topCatSphereIso n = TopCat.isoOfHomeo (SphereOddDegree.topCatSphereHomeomorph n)

Coercion simp lemmas

The homeomorphism topCatSphereHomeomorph and the categorical isomorphism topCatSphereIso are both the universe-ULift wrapper, so their underlying maps are ULift.down (forward) and ULift.up (backward). These rfl lemmas expose that to simp, letting downstream proofs evaluate the bridge maps on points.

@[simp]

theorem SphereOddDegree.topCatSphereHomeomorph_apply {n : ℕ} (x : ↑(TopCat.sphere n)) : (topCatSphereHomeomorph n) x = x.down

The forward homeomorphism TopCat.sphere n → Sphere n is ULift.down.

@[simp]

theorem SphereOddDegree.topCatSphereHomeomorph_symm_apply {n : ℕ} (y : Sphere n) : (topCatSphereHomeomorph n).symm y = { down := y }

The inverse homeomorphism Sphere n → TopCat.sphere n is ULift.up.

@[simp]

theorem SphereOddDegree.topCatSphereIso_hom_apply {n : ℕ} (x : ↑(TopCat.sphere n)) : (CategoryTheory.ConcreteCategory.hom (topCatSphereIso n).hom) x = x.down

The hom component of topCatSphereIso acts by ULift.down.

@[simp]

theorem SphereOddDegree.topCatSphereIso_inv_apply {n : ℕ} (y : Sphere n) : (CategoryTheory.ConcreteCategory.hom (topCatSphereIso n).inv) y = { down := y }

The inv component of topCatSphereIso acts by ULift.up.

theorem SphereOddDegree.topCatSphereIso_hom_eq {n : ℕ} : (topCatSphereIso n).hom = TopCat.ofHom ↑(topCatSphereHomeomorph n)

The hom of topCatSphereIso is TopCat.ofHom of the bundled homeomorphism (viewed as a continuous map). This identifies the categorical isomorphism with the homeomorphism at the level of TopCat morphisms.

theorem SphereOddDegree.topCatSphereIso_inv_eq {n : ℕ} : (topCatSphereIso n).inv = TopCat.ofHom ↑(topCatSphereHomeomorph n).symm

The inv of topCatSphereIso is TopCat.ofHom of the inverse homeomorphism (viewed as a continuous map).

Model transport of continuous maps to TopCat.sphere

Transport a continuous map between the raw sphere models into a TopCat morphism between the categorical sphere objects, by conjugating with topCatSphereIso. This is the general (possibly dimension-changing) form of the self-map transport used by the degree layer, and it is the basic input for feeding sphere maps to a TopCat-phrased (co)homology functor. It is functorial (toTopCatSphereMap_id, toTopCatSphereMap_comp) and is conjugate to the original map through the homeomorphisms (topCatSphereHomeomorph_toTopCatSphereMap).

noncomputable def SphereOddDegree.toTopCatSphereMap {n m : ℕ} (f : C(Sphere n, Sphere m)) : TopCat.sphere n ⟶ TopCat.sphere m

Transport a continuous map Sphere n → Sphere m to a morphism of the categorical sphere objects TopCat.sphere n ⟶ TopCat.sphere m, by conjugating with the bridge isomorphism topCatSphereIso.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SphereOddDegree.toTopCatSphereMap_apply {n m : ℕ} (f : C(Sphere n, Sphere m)) (x : ↑(TopCat.sphere n)) : (CategoryTheory.ConcreteCategory.hom (toTopCatSphereMap f)) x = { down := f x.down }

The transported morphism evaluates as f on the underlying points (modulo the ULift wrapper): it sends ULift.up x ↦ ULift.up (f x).

@[simp]

theorem SphereOddDegree.toTopCatSphereMap_id (n : ℕ) : toTopCatSphereMap (ContinuousMap.id (Sphere n)) = CategoryTheory.CategoryStruct.id (TopCat.sphere n)

The transport sends the identity continuous map to the identity morphism.

theorem SphereOddDegree.toTopCatSphereMap_comp {n m k : ℕ} (f : C(Sphere n, Sphere m)) (g : C(Sphere m, Sphere k)) : toTopCatSphereMap (g.comp f) = CategoryTheory.CategoryStruct.comp (toTopCatSphereMap f) (toTopCatSphereMap g)

The transport is functorial: it turns composition of continuous maps into composition of TopCat morphisms (in the same order).

theorem SphereOddDegree.topCatSphereHomeomorph_toTopCatSphereMap {n m : ℕ} (f : C(Sphere n, Sphere m)) (x : ↑(TopCat.sphere n)) : (topCatSphereHomeomorph m) ((CategoryTheory.ConcreteCategory.hom (toTopCatSphereMap f)) x) = f ((topCatSphereHomeomorph n) x)

Naturality of the transport with respect to the homeomorphism bridge: the transported morphism is conjugate to f through topCatSphereHomeomorph. This is the compatibility lemma a (co)homology functor consumes when comparing the induced map of toTopCatSphereMap f with that of f.