Working on the projective line

Stream: Is there code for X?

[Vincent Beffara]

I am trying to work on CP1 and to define charts, but so far my attempts at proving continuity have had limited success. Here is a minimal example of what I am trying to write:

import analysis.complex.basic
import linear_algebra.projective_space.basic

open projectivization

noncomputable theory

def CP1 := ℙ ℂ (ℂ × ℂ)

instance : topological_space CP1 := quotient.topological_space

def D : set CP1 := λ z, quotient.lift_on' z (λ w, w.val.2 ≠ 0) sorry

def f : CP1 → ℂ := λ z, quotient.lift_on' z (λ w, w.val.1 / w.val.2) sorry

lemma l5 : continuous_on f D :=
begin
  rw continuous_on_iff,
  rintro z hz t ht hzt,
  refine ⟨f ⁻¹' t ∩ D, _, _, _⟩,
  { simp [is_open_coinduced, ← set.preimage_comp, set.preimage, f, set.mem_def, D],
    simp [is_open_induced_iff],
    use {z : ℂ × ℂ | z.1 / z.2 ∈ t ∧ z.2 ≠ 0},
    sorry
  },
  { sorry },
  { sorry }
end

I am using lift_on' everywhere because for other parts it has been easier than using rep (i.e., quotient.out if I tracked it right), but as far as I can tell it is not the source of my issue. Do we need a restricted version of docs#continuous_quotient_lift_on' somewhere?

[Junyan Xu]

Not familiar with the continuity library but mathlib already has docs#projectivization (Zulip thread).

[Yaël Dillies]

I believe this is what Vincent is using already.

[Junyan Xu]

Oh yes indeed! Sorry for my oversight.

[Vincent Beffara]

I am using it, but there does not seem to be a lot of API yet there

[Adam Topaz]

I think a nicer approach would be to take a perfect pairing of vector spaces $V \times W \to k$ and use that to construct affine charts. E.g. this lets you identify the projectivization of $W$ with the dual projective space of $V$, so points in the projectivization of $W$ correspond to hyperplanes in the projective space of $V$, and their complements give you affine charts. This would make the situation much more symmetric, which will probably simplify a lot of things (similar to @Heather Macbeth ‘s approach to the sphere). I should also mention that I have a student @Michael Blyth who will build up some of the API around projective spaces as a summer project.

[Adam Topaz]

(Of course, this is still orthogonal to the question asked regarding continuous_on…)

[Oliver Nash]

And let's not forget connecting to docs#algebraic_geometry.Proj.to_LocallyRingedSpace !

[Junyan Xu]

projectivization should be generalized to division rings, and there's also OP^2, then we can define all the Hopf fibrations.

[Oliver Nash]

I agree projectivization should be generalised to division_rings but we won't get $\mathbb{OP}^2$ that way. Indeed there is no such thing as $\mathbb{OP}^k$ for $k > 2$ so I'd say that case will have to be ad hoc.

[Adam Topaz]

I tried making that generalization when I defined the projectivization originally, but I got bogged down with a lot of the finite_dimensional stuff being done only in the commutative case.

[Adam Topaz]

Once the finite dimensional stuff is generalized, it should be very quick to generalize the assumptions on projectivization

[Junyan Xu]

recent developments like #13870 #13845 seems relevant

[Vincent Beffara]

OK so I finally made it, and it is not too ugly in the end:

import analysis.complex.basic
import linear_algebra.projective_space.basic

open projectivization

noncomputable theory

def CP1 := ℙ ℂ (ℂ × ℂ)

instance : topological_space CP1 := quotient.topological_space

def D : set CP1 := λ z, quotient.lift_on' z (λ w, w.val.2 ≠ 0) sorry

def f : CP1 → ℂ := λ z, quotient.lift_on' z (λ w, w.val.1 / w.val.2) sorry

lemma l5 : continuous_on f D :=
begin
  rw continuous_on_iff,
  rintro z hz t ht hzt,
  refine ⟨f ⁻¹' t ∩ D, _, by simp [hz, hzt], _⟩,
  { refine ⟨{z | z.1 / z.2 ∈ t ∧ z.2 ≠ 0}, _, rfl⟩,
    rw [set.set_of_and, set.inter_comm],
    refine continuous_on.preimage_open_of_open _ _ ht,
    { apply continuous_on.div,
      { exact continuous_fst.continuous_on },
      { exact continuous_snd.continuous_on },
      { simp only [set.mem_set_of_eq, imp_self, forall_const] } },
    { exact is_open.preimage continuous_snd is_open_compl_singleton } },
  { simp [set.inter_assoc, set.inter_subset_left] }
end

(the sorrys in the definitions are not a problem). All in all I have a local_homeomorph (ℙ ℂ (ℂ × ℂ)) ℂ, built in an ad hoc way but it should be usable even if it doesn't win any beauty contest.

[Junyan Xu]

I think a general approach is to compose the continuous map from C^n to C^(n+1) (sending one coordinate to 1) with the quotient map C^(n+1)\{0} → CP^n to get an injective map C^n → CP^n whose inverse is your f. Restricted to each closed ball, it's an injective continuous map from compact to Hausdorff, hence an homeomorphism onto its image, so f is continuous on the image. You still need to show that CP^n is Hausdorff (t2_space) though.

[Vincent Beffara]

Indeed that was my other option (docs#is_open_map.continuous_on_image_of_left_inv_on) but my f was simple enough that I thought it would be easy, and that was the opening of this particular rabbit hole. You are certainly right that in all generality it will be easier to work with the inverse map.

[Junyan Xu]

Hmm, it seems you still have to show that the image contains an open neighborhood of the point around which you want to find a chart. So maybe this approach isn't that simpler after all. (simply showing is_open_map bypasses all these compact Hausdorff argument)

[Vincent Beffara]

So here is a definition of the manifold structure on the Riemann sphere / CP1. It has all kinds of problems and I am not going to PR it anytime soon, but I am putting it here for future reference, and if possible for comments :-)

import analysis.complex.basic
import geometry.manifold.charted_space
import geometry.manifold.smooth_manifold_with_corners
import linear_algebra.projective_space.basic
import topology.constructions

noncomputable theory

open_locale manifold

namespace projectivization

abbreviation C'2 := {z : ℂ × ℂ // z ≠ 0}
abbreviation CP1 := ℙ ℂ (ℂ × ℂ)

local notation `[`x`:`y`, `h`]` := (mk ℂ (x,y) h : CP1)
local notation `[`x`:`y`]` := [x:y, by simp]

instance : topological_space CP1 := quotient.topological_space

/- General-purpose lemmas (not about projectivization itself) -/

lemma is_open_preimage_div {t : set ℂ} (ht : is_open t) :
  is_open {z : ℂ × ℂ | z.2 ≠ 0 ∧ z.1 / z.2 ∈ t} :=
(continuous_fst.continuous_on.div continuous_snd.continuous_on (λ _, id)).preimage_open_of_open
  (is_open_compl_singleton.preimage continuous_snd) ht

/- Technical lemmas about projectivization -/

lemma mk_eq_mk_iff_mul_eq_mul {x y : ℂ × ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
  mk ℂ x hx = mk ℂ y hy ↔ x.1 * y.2 = x.2 * y.1 :=
begin
  rw [mk_eq_mk_iff],
  split,
  { rintro ⟨a, rfl⟩,
    simp [units.smul_def, mul_assoc, mul_comm y.1 _] },
  { intro hxy,
    rcases x with ⟨x1, x2⟩,
    rcases y with ⟨y1, y2⟩,
    by_cases y1 = 0,
    { simp only [h, ne.def, prod.mk_eq_zero, eq_self_iff_true, true_and] at hy,
      simp only [h, hy, mul_zero, mul_eq_zero, or_false] at hxy,
      simp only [hxy, ne.def, prod.mk_eq_zero, eq_self_iff_true, true_and] at hx,
      use units.mk0 (x2/y2) (div_ne_zero hx hy),
      simp [units.smul_def, h, hy, hxy] },
    { by_cases h' : x1 = 0,
      { simp only [h', ne.def, prod.mk_eq_zero, eq_self_iff_true, true_and] at hx,
        simp only [h', hx, h, zero_mul, zero_eq_mul, false_or] at hxy,
        contradiction },
      { use units.mk0 (x1/y1) (div_ne_zero h' h),
        simp [units.smul_def, div_mul_cancel, h, mul_comm_div', ← mul_div_assoc, hxy] } } }
end

lemma div_eq_div_of_mk_eq_mk {x y : ℂ × ℂ} (hx : x ≠ 0) (hy : y ≠ 0) (h : mk ℂ x hx = mk ℂ y hy) :
  x.1 / x.2 = y.1 / y.2 :=
begin
  rcases (mk_eq_mk_iff _ _ _ _ _).mp h with ⟨a, rfl⟩,
  simp [units.smul_def, mul_div_mul_left]
end

@[simp] lemma lift_on_mk {α : Type*} {z : ℂ × ℂ} {h : z ≠ 0} {f : C'2 → α} {hf} :
  quotient.lift_on' (mk ℂ z h) f hf = f ⟨z, h⟩ := rfl

/- Topological results -/

instance : t1_space CP1 :=
begin
  refine ⟨λ x, _⟩,
  induction x using projectivization.ind with x hx,
  rw ← is_open_compl_iff,
  change is_open {z | ¬ mk' ℂ z = mk ℂ x hx},
  simp_rw [mk'_eq_mk, mk_eq_mk_iff_mul_eq_mul],
  have hc : continuous (λ z : C'2, z.val.1 * x.2 - z.val.2 * x.1) := by continuity,
  convert ← is_open_compl_singleton.preimage hc,
  ext,
  exact sub_ne_zero
end

/- Chart constructions -/

def rec1 (z : CP1) : ℂ :=
quotient.lift_on' z (λ w, w.val.1 / w.val.2)
  (λ x y h, div_eq_div_of_mk_eq_mk x.prop y.prop (quotient.eq'.mpr h))

lemma continuous_rec1 : continuous_on rec1 {[1:0]}ᶜ :=
begin
  rw continuous_on_iff,
  rintro z hz t ht hzt,
  refine ⟨rec1 ⁻¹' t ∩ {[1:0]}ᶜ, _, ⟨hzt, hz⟩, by simp [set.inter_assoc, set.inter_subset_left]⟩,
  refine ⟨{z | z.2 ≠ 0 ∧ z.1 / z.2 ∈ t}, is_open_preimage_div ht, _⟩,
  ext ⟨x, hx⟩,
  simp only [rec1, and_comm _ (_ ∈ t), not_iff_not, set.mem_set_of_eq, subtype.coe_mk,
    set.mem_inter_eq, set.mem_preimage, quotient.lift_on'_mk, set.mem_compl_eq,
    set.mem_singleton_iff, and.congr_right_iff],
  change _ → (_ ↔ mk ℂ x hx = _),
  simp [mk_eq_mk_iff_mul_eq_mul, eq_comm]
end

def lh1 : local_homeomorph CP1 ℂ :=
{
  to_fun := rec1,
  inv_fun := λ z, [z:1],
  source := {[1:0]}ᶜ,
  target := set.univ,

  map_source' := λ _ _, set.mem_univ _,
  map_target' := by simp [mk_eq_mk_iff_mul_eq_mul],

  left_inv' := λ z hz, by {
    induction z using projectivization.ind with z h,
    simp only [set.mem_compl_iff, set.mem_singleton_iff, mk_eq_mk_iff_mul_eq_mul, mul_zero, mul_one,
      ← ne.def] at hz,
    simp [rec1, mk_eq_mk_iff_mul_eq_mul, hz.symm] },
  right_inv' := by simp [rec1],

  open_source := is_open_compl_singleton,
  open_target := is_open_univ,
  continuous_to_fun := continuous_rec1,
  continuous_inv_fun := by {
    apply continuous.continuous_on,
    apply continuous_quot_mk.comp,
    continuity },
}

@[simp] lemma l1 {z : ℂ × ℂ} : z.swap = 0 ↔ z = 0 :=
by { rcases z with ⟨x, y⟩, simp [and_comm] }

def antip : CP1 → CP1 := λ z, quotient.lift_on' z
  (λ w, mk ℂ w.val.swap (by simp [w.prop]))
begin
  rintro ⟨⟨x1, x2⟩, hx⟩ ⟨⟨y1, y2⟩, hy⟩ hxy,
  simp [mk_eq_mk_iff_mul_eq_mul, (mk_eq_mk_iff_mul_eq_mul hx hy).mp (quotient.eq'.mpr hxy)]
end

lemma antip.involutive : function.involutive antip :=
begin
  intro z,
  induction z using projectivization.ind with z h,
  simp [antip]
end

lemma antip.continuous : continuous antip :=
begin
  apply continuous_quotient_lift_on',
  apply continuous_quotient_mk.comp,
  apply continuous_subtype_mk,
  exact continuous_swap.comp continuous_subtype_val,
end

def antipode : homeomorph CP1 CP1 :=
{
  to_fun := antip,
  inv_fun := antip,
  left_inv := antip.involutive,
  right_inv := antip.involutive,
  continuous_to_fun := antip.continuous,
  continuous_inv_fun := antip.continuous
}

lemma antip_infty : antip [1:0] = [0:1] := by simp [antip]

def lh2 : local_homeomorph CP1 ℂ :=
antipode.to_local_homeomorph.trans lh1

instance : charted_space ℂ CP1 :=
{
  atlas := {lh1, lh2},
  chart_at := λ z, by { by_cases z = [1:0], exact lh2, exact lh1 },
  mem_chart_source := λ z,
    by { by_cases z = [1:0]; simp [h, lh1, lh2, antipode, antip, mk_eq_mk_iff_mul_eq_mul] },
  chart_mem_atlas := λ z, by { by_cases z = [1:0]; simp [h] }
}

lemma invC1 : cont_diff_on ℂ ⊤ (λ z, z⁻¹) ({0}ᶜ : set ℂ) :=
cont_diff_on_inv ℂ

@[simp] lemma dom1 : lh1.target ∩ lh1.symm ⁻¹' lh2.source = {0}ᶜ :=
begin
  ext,
  simp [lh1, lh2, antipode, antip, mk_eq_mk_iff_mul_eq_mul, eq_comm],
end

@[simp] lemma dom2 : lh2.target ∩ lh2.symm ⁻¹' lh1.source = {0}ᶜ :=
begin
  ext,
  simp [lh1, lh2, antipode, antip, mk_eq_mk_iff_mul_eq_mul, eq_comm],
end

instance : smooth_manifold_with_corners 𝓘(ℂ) CP1 :=
smooth_manifold_with_corners_of_cont_diff_on 𝓘(ℂ) CP1
begin
  rintro e e' (rfl|he) (rfl|he'),
  { simp [cont_diff_on_id.congr, lh1, rec1] },
  { simp at he',
    simp [he'],
    exact invC1.congr (by simp [lh1, lh2, antipode, antip, rec1]) },
  { simp at he,
    simp [he],
    exact invC1.congr (by simp [lh1, lh2, antipode, antip, rec1]) },
  { simp at he he',
    simp [cont_diff_on_id.congr, lh1, lh2, he, he', rec1] }
end

end projectivization

[Vincent Beffara]

@Adam Topaz I totally agree that this is not the correct way to do it, more of a learning exercise...

[Vincent Beffara]

@Adam Topaz sorry for pinging you, do you have comments on my PR #14059 that adds some API to projective/basic.lean? I am mostly wondering about two things:

• the choice of k \times k as opposed to fin 2 \to k as the underlying space: fin n would be the natural generalization here, OTOH there is a lot of special-casing for projective lines and using k \times k for that case felt more natural;
• then the addition of normalizing simp lemmas into the projectivization.mk form: this in my experience made things smoother to use, especially since some lemmas made some quotient.mk and quotient.mk' terms appear, but unfortunately it broke two of your proofs that relied on by simp [mk] so I thought I should let you know.

What do you think?

[Johan Commelin]

Ideally we would have a smooth API to work with vector spaces with a given basis (of size 2, or 3, or n).

[Adam Topaz]

I do think it would be better to come up with a more uniform way to do this for an arbitrary (finite dimensional) vector space.

[Adam Topaz]

Concerning projectivization.mk, that seems fine to me, but my one (small) concern is that it might require duplicating more of the quotient api.

[Adam Topaz]

BTW your mk_eq_mk_iff_mul_eq_mul can be generalized as follows (the following proof is very golfable)

import linear_algebra.projective_space.basic
import tactic

open projectivization
variables (K : Type*) [field K]
lemma foobar {α : Type*} (x y : (α → K)) (hx : x ≠ 0) (hy : y ≠ 0) :
  mk K x hx = mk K y hy ↔ ∀ i j : α, x i * y j = x j * y i :=
begin
  split,
  { intros h i j,
    rw mk_eq_mk_iff at h,
    obtain ⟨a,rfl⟩ := h,
    erw [pi.smul_apply, pi.smul_apply],
    simp only [smul_eq_mul, mul_assoc, mul_comm (y i)] },
  { intros h,
    have : ∃ j : α, y j ≠ 0,
    { contrapose! hy, ext j, rw hy, refl },
    obtain ⟨j,hj⟩ := this,
    have hj' : x j ≠ 0,
    { intros c,
      apply hx, ext i, specialize h i j,
      dsimp,
      rw [c, zero_mul] at h,
      apply_fun (λ e, e * (y j)⁻¹) at h,
      field_simp at h,
      assumption },
    rw mk_eq_mk_iff,
    use ((units.mk0 (x j) hj') * (units.mk0 (y j) hj)⁻¹),
    ext i,
    erw [pi.smul_apply, smul_eq_mul],
    push_cast,
    rw [mul_comm, ← mul_assoc, mul_comm, ← smul_eq_mul],
    dsimp,
    field_simp,
    rw mul_comm (y i), apply h }
end