@[reducible, inline]

abbrev RealProjectiveSpace.Sphere (n : ℕ) : Type

The unit $n$-sphere $S^n \subset \mathbb{R}^{n+1}$, defined as the metric sphere of radius $1$ in $\mathbb{R}^{n+1}$.

def RealProjectiveSpace.antipodalSetoid (n : ℕ) : Setoid (Sphere n)

The antipodal equivalence on $S^n$: $x \sim y$ iff $y = x$ or $y = -x$. The quotient by this relation is real projective space $\mathbf{RP}^n$.

def RealProjectiveSpace.RPn (n : ℕ) : Type

Real projective $n$-space $\mathbf{RP}^n = S^n / \{\pm 1\}$, the quotient of $S^n$ by the antipodal action.

@[implicit_reducible]

instance RealProjectiveSpace.instTopologicalSpaceRPn (n : ℕ) : TopologicalSpace (RPn n)

$\mathbf{RP}^n$ carries the quotient topology inherited from $S^n$.

def RealProjectiveSpace.homologyGroup (n k : ℕ) : AddCommGrpCat

Proposition 17.1. The integral singular homology of real projective $n$-space: $H_0(\mathbf{RP}^n) = \mathbb{Z}$, $H_n(\mathbf{RP}^n) = \mathbb{Z}$ if $n$ is odd, $H_k(\mathbf{RP}^n) = \mathbb{Z}/2$ for odd $k$ with $0 < k < n$, and zero otherwise.

def RealProjectiveSpace.rpnImageSubgroup (n k : ℕ) : AddSubgroup ℤ

The image subgroup of the cellular differential $\partial_{k+1} : C_{k+1}(\mathbf{RP}^n) \to C_k(\mathbf{RP}^n) \cong \mathbb{Z}$: all of $\mathbb{Z}$ when $k > n$, zero when $k = n$ or $k$ is even with $k < n$, and $2\mathbb{Z}$ when $k$ is odd with $k < n$.

def RealProjectiveSpace.rpnChainHomology (n k : ℕ) : AddCommGrpCat

The cellular chain homology of $\mathbf{RP}^n$ in degree $k$, computed as $\mathbb{Z} / \text{(image of }\partial_{k+1}\text{)}$.

theorem RealProjectiveSpace.rpnImageSubgroup_zero (n : ℕ) : rpnImageSubgroup n 0 = ⊥

In degree $0$, the image subgroup is trivial: $\partial_1 = 0$ on $C_0(\mathbf{RP}^n)$.

theorem RealProjectiveSpace.rpnImageSubgroup_odd_lt {n k : ℕ} (hk : Odd k) (hkn : k < n) : rpnImageSubgroup n k = AddSubgroup.zmultiples 2

For odd $k$ with $k < n$, the image of $\partial_{k+1}$ is $2\mathbb{Z}$ (so $H_k = \mathbb{Z}/2$).

theorem RealProjectiveSpace.rpnImageSubgroup_self (n : ℕ) : rpnImageSubgroup n n = ⊥

In the top degree $k = n$, the image of $\partial_{n+1} = 0$ is trivial.

def RealProjectiveSpace.rpnChainHomology_iso_homologyGroup (n k : ℕ) : rpnChainHomology n k ≅ homologyGroup n k

The chain-level homology of $\mathbf{RP}^n$ matches the explicit description in homologyGroup.

def RealProjectiveSpace.sphereNeg (n : ℕ) (x : Sphere n) : Sphere n

The antipodal map $x \mapsto -x$ on $S^n$.

theorem RealProjectiveSpace.sphereNeg_val (n : ℕ) (x : Sphere n) : ↑(sphereNeg n x) = -↑x

Unfold the underlying vector of the antipodal map.

theorem RealProjectiveSpace.sphereNeg_involutive (n : ℕ) : Function.Involutive (sphereNeg n)

The antipodal map on $S^n$ is an involution.

theorem RealProjectiveSpace.continuous_sphereNeg (n : ℕ) : Continuous (sphereNeg n)

The antipodal map on $S^n$ is continuous.

def RealProjectiveSpace.sphereNegHomeomorph (n : ℕ) : Sphere n ≃ₜ Sphere n

The antipodal map as a self-homeomorphism of $S^n$.

theorem RealProjectiveSpace.isOpenMap_rpn_mk (n : ℕ) : IsOpenMap (Quotient.mk (antipodalSetoid n))

The quotient map $S^n \to \mathbf{RP}^n$ is open: the saturation $U \cup (-U)$ of an open set is open.

theorem RealProjectiveSpace.isOpenQuotientMap_rpn_mk (n : ℕ) : IsOpenQuotientMap (Quotient.mk (antipodalSetoid n))

Combining surjectivity, continuity, and openness: $S^n \to \mathbf{RP}^n$ is an open quotient map.

theorem RealProjectiveSpace.isClosed_antipodal_rel (n : ℕ) : IsClosed {p : Sphere n × Sphere n | ⟦p.1⟧ = ⟦p.2⟧}

The antipodal equivalence relation on $S^n \times S^n$ is closed: $\{(x, y) : x = \pm y\}$ is a union of two closed graphs.

theorem RealProjectiveSpace.rpn_t2Space (n : ℕ) : T2Space (RPn n)

$\mathbf{RP}^n$ is Hausdorff: the open quotient map by a closed equivalence relation gives a Hausdorff quotient.

def RealProjectiveSpace.RPnCell (n k : ℕ) : Type

Index type for the CW cells of $\mathbf{RP}^n$ in degree $k$: a single cell when $k \le n$, none otherwise.

instance RealProjectiveSpace.RPnCell.finite (n k : ℕ) : Finite (RPnCell n k)

Each $\mathbf{RP}^n$ cell-index type is finite.

def RealProjectiveSpace.rpnRawVec (n k : ℕ) (_hk : k ≤ n) (x : Fin k → ℝ) : EuclideanSpace ℝ (Fin (n + 1))

Auxiliary vector in $\mathbb{R}^{n+1}$ used to define the $k$-cell characteristic map: $x \in B^k$ (i.e.\ first $k$ coordinates) gets extended by $1 - \|x\|$ in the $k$th slot and zeros afterwards.

theorem RealProjectiveSpace.rpnRawVec_apply (n k : ℕ) (hk : k ≤ n) (x : Fin k → ℝ) (i : Fin (n + 1)) : (rpnRawVec n k hk x).ofLp i = if h : ↑i < k then x ⟨↑i, h⟩ else if ↑i = k then 1 - ‖x‖ else 0

Component formula for rpnRawVec: the $i$th coordinate is $x_i$ for $i < k$, $1 - \|x\|$ for $i = k$, and $0$ for $i > k$.

theorem RealProjectiveSpace.rpnRawVec_ne_zero (n k : ℕ) (hk : k ≤ n) (x : Fin k → ℝ) : rpnRawVec n k hk x ≠ 0

The auxiliary vector rpnRawVec is never zero (so its normalisation is well-defined).

noncomputable def RealProjectiveSpace.rpnCharMapFwd (n k : ℕ) (hk : k ≤ n) (x : Fin k → ℝ) : RPn n

The forward characteristic map $B^k \to \mathbf{RP}^n$ of the $k$-cell: normalize the auxiliary vector and project to $\mathbf{RP}^n$.

noncomputable def RealProjectiveSpace.rpnCharMapInv (n k : ℕ) (hk : k ≤ n) (q : RPn n) : Fin k → ℝ

The inverse to the characteristic map on the open cell: extracts the first $k$ coordinates of the representative, with a sign and normalisation depending on the $k$th coordinate.

def RealProjectiveSpace.rpnOpenCell (n k : ℕ) (hk : k ≤ n) : Set (RPn n)

The open $k$-cell in $\mathbf{RP}^n$: points representable by a sphere element whose coordinates above index $k$ vanish and whose coordinate at index $k$ is nonzero.

theorem RealProjectiveSpace.rpnCharMapInv_mem_ball (n k : ℕ) (hk : k ≤ n) (q : RPn n) (hq : q ∈ rpnOpenCell n k hk) : ‖rpnCharMapInv n k hk q‖ < 1

The image of the inverse characteristic map lies in the open unit ball of $\mathbb{R}^k$.

theorem RealProjectiveSpace.rpnCharMap_leftInv (n k : ℕ) (hk : k ≤ n) (x : Fin k → ℝ) (hx : ‖x‖ < 1) : rpnCharMapInv n k hk (rpnCharMapFwd n k hk x) = x

The forward characteristic map followed by the inverse recovers $x$ for $\|x\| < 1$.

theorem RealProjectiveSpace.rpnCharMap_rightInv (n k : ℕ) (hk : k ≤ n) (q : RPn n) (hq : q ∈ rpnOpenCell n k hk) : rpnCharMapFwd n k hk (rpnCharMapInv n k hk q) = q

The inverse characteristic map followed by the forward map recovers $q$ for points in the open cell.

noncomputable def RealProjectiveSpace.rpnCharMap (n k : ℕ) (i : RPnCell n k) : PartialEquiv (Fin k → ℝ) (RPn n)

The characteristic map of the $k$-cell, packaged as a PartialEquiv between the open unit ball in $\mathbb{R}^k$ and the open cell in $\mathbf{RP}^n$.

theorem RealProjectiveSpace.rpnCharMap_source (n k : ℕ) (i : RPnCell n k) : (rpnCharMap n k i).source = Metric.ball 0 1

The source of the characteristic partial equivalence is the open unit ball in $\mathbb{R}^k$.

theorem RealProjectiveSpace.rpnCharMap_continuousOn (n k : ℕ) (i : RPnCell n k) : ContinuousOn (↑(rpnCharMap n k i)) (Metric.closedBall 0 1)

The characteristic map of each cell is continuous on the closed unit ball.

theorem RealProjectiveSpace.rpnCharMap_continuousOn_symm (n k : ℕ) (i : RPnCell n k) : ContinuousOn (↑(rpnCharMap n k i).symm) (rpnCharMap n k i).target

The inverse characteristic map is continuous on the open cell.

theorem RealProjectiveSpace.rpnCharMap_pairwiseDisjoint (n : ℕ) : Set.univ.PairwiseDisjoint fun (ni : (k : ℕ) × RPnCell n k) => ↑(rpnCharMap n ni.fst ni.snd) '' Metric.ball 0 1

The open cells of different dimensions in $\mathbf{RP}^n$ are pairwise disjoint.

theorem RealProjectiveSpace.rpnCharMap_mapsTo (n k : ℕ) (i : RPnCell n k) : Set.MapsTo (↑(rpnCharMap n k i)) (Metric.sphere 0 1) (⋃ (m : ℕ), ⋃ (_ : m < k), ⋃ (j : RPnCell n m), ↑(rpnCharMap n m j) '' Metric.closedBall 0 1)

The boundary $\partial B^k$ under the characteristic map lies in the union of all lower skeleta of $\mathbf{RP}^n$.

theorem RealProjectiveSpace.rpnCharMap_union (n : ℕ) : ⋃ (k : ℕ), ⋃ (j : RPnCell n k), ↑(rpnCharMap n k j) '' Metric.closedBall 0 1 = Set.univ

The closed cells cover $\mathbf{RP}^n$ entirely.

noncomputable def RealProjectiveSpace.rpn_cwComplex (n : ℕ) : Topology.CWComplex Set.univ

The finite CW-complex structure on $\mathbf{RP}^n$ with one cell in each dimension $0 \le k \le n$, packaged using Topology.CWComplex.mkFinite.

noncomputable def RealProjectiveSpace.rpn_skeletonHomology_succ_iso_chainHomology (n k : ℕ) : CWHomology.skeletonHomology (RPn n) (k + 1) k ≅ rpnChainHomology n k

The skeletal homology in adjacent degrees of the $\mathbf{RP}^n$ CW-complex agrees with the cellular chain homology rpnChainHomology.

noncomputable def RealProjectiveSpace.rpnSkeletonSC_homology_iso_rpnChainHomology (n k : ℕ) : { X₁ := CWHomology.relHomologySkeleton (RPn n) (k + 1) (k + 1), X₂ := CWHomology.skeletonHomology (RPn n) k k, X₃ := CWHomology.skeletonHomology (RPn n) (k + 1) k, f := CWHomology.skeletonConnectingHom (RPn n) k, g := CWHomology.skeletonStepMap (RPn n) k, zero := ⋯ }.homology ≅ rpnChainHomology n k

The homology of the skeletal short complex of $\mathbf{RP}^n$ at index $k$ agrees with the explicit cellular chain homology rpnChainHomology n k.

noncomputable def RealProjectiveSpace.rpnCellularHomology_iso_rpnChainHomology (n k : ℕ) : CWHomology.cellularHomologyGroup k (RPn n) ≅ rpnChainHomology n k

The cellular homology of $\mathbf{RP}^n$ matches the explicit cellular chain homology rpnChainHomology.

theorem RealProjectiveSpace.rpn_homology_gt (n k : ℕ) (hkn : k > n) : CategoryTheory.Limits.IsZero (CWHomology.cellularHomologyGroup k (RPn n))

$\mathbf{RP}^n$ has no cellular homology above the top dimension: $H_k = 0$ for $k > n$.

noncomputable def RealProjectiveSpace.rpnSingularIsoChainHomology (n k : ℕ) : AlgebraicTopologyI.SingularHomologyGroup k (RPn n) ≅ rpnChainHomology n k

Transfer the CW $=$ singular homology comparison to identify singular homology of $\mathbf{RP}^n$ with the explicit rpnChainHomology.

noncomputable def RealProjectiveSpace.homology_rpn (n k : ℕ) : AlgebraicTopologyI.SingularHomologyGroup k (RPn n) ≅ homologyGroup n k

Proposition 17.1 (formal statement). The singular homology of $\mathbf{RP}^n$ is given by the explicit homologyGroup: $H_0 = \mathbb{Z}$, $H_n = \mathbb{Z}$ for $n$ odd, $H_k = \mathbb{Z}/2$ for odd $k < n$, and zero otherwise.