Quotient.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The metric quotient of the round four-sphere by a free involution

The orientation double cover in the manuscript's unoriented argument has a free isometric deck involution. Once that cover is identified with the round sphere, its metric quotient is the concrete real projective model below.

theorem OAI.PositiveEinsteinFour.free_round_involution_quotient_equiv line 20

Source documentation

Identification of quotient fibers supplies an equivalence that sends the quotient projection to the standard projectivization map.

theorem free_round_involution_quotient_equiv
    {M : Type*}
    (τ : RoundSphere4 → RoundSphere4)
    (hτ : Function.Involutive τ)
    (hτdistance : ∀ x y, roundDistance (τ x) (τ y) = roundDistance x y)
    (hτfree : ∀ x, τ x ≠ x)
    (p : RoundSphere4 → M) (hp : Function.Surjective p)
    (hfibers : ∀ x y, p x = p y ↔ x = y ∨ x = τ y) :
    ∃ e : M ≃ RealProjective4, ∀ x, e (p x) = sphereToProjective x := by
…

theorem OAI.PositiveEinsteinFour.free_round_involution_quotient_is_projective line 55

Source documentation

A two-sheeted metric quotient of the round four-sphere by a free isometric involution is equivalent to RealProjective4, with its stated model distance. The quotient fibers and quotient-distance formula are explicit hypotheses; the construction also identifies the quotient map with projectivization.

theorem free_round_involution_quotient_is_projective
    {M : Type*} (dM : M → M → ℝ)
    (τ : RoundSphere4 → RoundSphere4)
    (hτ : Function.Involutive τ)
    (hτdistance : ∀ x y, roundDistance (τ x) (τ y) = roundDistance x y)
    (hτfree : ∀ x, τ x ≠ x)
    (p : RoundSphere4 → M) (hp : Function.Surjective p)
    (hfibers : ∀ x y, p x = p y ↔ x = y ∨ x = τ y)
    (hdistance : ∀ x y,
      dM (p x) (p y) = min (roundDistance x y) (roundDistance x (τ y))) :
    ∃ e : M ≃ RealProjective4,
      (∀ x, e (p x) = sphereToProjective x) ∧
…

theorem OAI.PositiveEinsteinFour.scaled_round_involution_quotient_is_projective line 81

Source documentation

The quotient identification directly supplies the scaled metric conclusion used by the classification statement. No sign assumption on a is needed for this implication: the caller separately supplies positivity of the scale.

theorem scaled_round_involution_quotient_is_projective
    {M : Type*} [TopologicalSpace M] [ChartedSpace FourSpace M]
    [IsManifold I4 ∞ M]
    (g : SmoothMetric M) (a : ℝ)
    (τ : RoundSphere4 → RoundSphere4)
    (hτ : Function.Involutive τ)
    (hτdistance : ∀ x y, roundDistance (τ x) (τ y) = roundDistance x y)
    (hτfree : ∀ x, τ x ≠ x)
    (p : RoundSphere4 → M) (hp : Function.Surjective p)
    (hfibers : ∀ x y, p x = p y ↔ x = y ∨ x = τ y)
    (hdistance : ∀ x y, scaledEDistance g a (p x) (p y) =
      ENNReal.ofReal (min (roundDistance x y) (roundDistance x (τ y)))) :
…