Hopf fibration

Stream: LftCM22

[Jeremy Avigad]

I managed to define the Hopf fibration as a function from S^3 to S^2. I didn't even have to think about the calculation. polyrith is great!

@Heather Macbeth, maybe tomorrow or Thursday you can help my project group and anyone else interested understand how to show that this is a smooth map between the manifolds. The API is scary to me.

import geometry.manifold.instances.sphere
import data.polynomial.basic
import tactic.polyrith

noncomputable theory
open complex
open metric

/-
The relevant function from ℂ × ℂ to ℂ × ℝ is given by

 (z, w) ↦ (2 w* z, |z|^2 - |w|^2),

 i.e.

  (a + bi, c + di) ↦ (2 (ac + bd) + 2(bc-ad)i, a^2 + b^2 - (c^2 + d^2))

First, we express this as a function from ℝ^4 to ℝ^3.
-/

def hopf_fn (v : euclidean_space ℝ (fin 4)) : euclidean_space ℝ (fin 3) :=
![ 2 * (v 0 * v 2 + v 1 * v 3), 2 * (v 1 * v 2 - v 0 * v 3),  (v 0)^2 + (v 1)^2 - (v 2)^2 - (v 3)^2]

/-
Then we show that it takes elements of S^3 maps to S^2.
We extract the relevant calculation for `polyrith`.
-/

theorem useful {v0 v1 v2 v3 : ℝ} (h : v0^2 + v1^2 + v2^2 + v3^2 = 1) :
  (2 * (v0 * v2 + v1 * v3))^2 + (2 * (v1 * v2 - v0 * v3))^2 + (v0^2 + v1^2 - v2^2 - v3^2)^2 = 1 :=
by { linear_combination (1 * v0 ^ 2 + 1 * v2 ^ 2 + 1 * v1 ^ 2 + 1 * v3 ^ 2 + 1) * h }

def hopf_map (v : sphere (0 : euclidean_space ℝ (fin 4)) 1) :
  sphere (0 : euclidean_space ℝ (fin 3)) 1 :=
⟨ hopf_fn v,
  begin
    have := v.property,
    simp [- norm_eq_of_mem_sphere, euclidean_space.norm_eq, finset.sum_fin_eq_sum_range, finset.sum_range_succ] at this,
    simp [hopf_fn, euclidean_space.norm_eq, finset.sum_fin_eq_sum_range, finset.sum_range_succ],
    rw if_pos, swap, norm_num,
    exact useful this
  end ⟩

[Anatole Dedecker]

I guess polyrith will be the new linarith : people will come to complain that it doesn't solve their goal

[Heather Macbeth]

@Jeremy Avigad Nice!! Yes, let's meet. I'm meeting with a different project at the start of the code review session tomorrow, how about we meet at 11:45?

[Junyan Xu]

Wikipedia has definitions of Hopf fibrations over the reals, complexes, quaternions (in arbitrary dimensions), and octonions (in dim 1 and 2). I think this is the generality we should aim for; the classical Hopf fibration S^3 → S^2 is realized as S^3 ⊆ C^2\{0} → CP^1 composed with a homeomorphism CP^1 → S^2 (probably stereographic projection from a pole?).

Since docs#projectivization hasn't been generalized to division rings, we should be content with the real and complex versions for now. Defining the smooth manifold structure on RP^n and CP^n would be a nice first project (and it's already done for CP^1) and exhibiting the diffeomorphism between CP^1 and S^2 would be another (where polyrith could be useful; maybe it will also be useful in dealing with inversion in spheres (e.g. in #14703), and isometry between / isometry group of different models of the hyperbolic space).

[Heather Macbeth]

@Junyan Xu I suggested this explicit version of the Hopf fibration as a project. But I agree, the smooth manifold structure on $\mathbb{P}^n$ should eventually be added -- I would take a more co-ordinate free approach than the quickie code you linked for the Riemann sphere, though. We should have charts centred at any point, not just $n+1$ charts. Happy to talk to anyone interested here!

[Sam Freedman]

I'm also interested in discussing the right level of formalization for this project. It'd be cool to get as many of the Hopf fibrations at once.
I'm also wondering if it's possible to prove that the Hopf fibration is a nontrivial fiber bundle with fiber/base/total space being spheres. https://leanprover-community.github.io/mathlib_docs/topology/fiber_bundle.html#top
Happy to chat at 11:45 or earlier.

[Sam Freedman]

import geometry.manifold.instances.sphere
import data.polynomial.basic
import data.polynomial.eval
import tactic.polyrith
import analysis.inner_product_space.pi_L2
import analysis.calculus.cont_diff

noncomputable theory
open complex
open metric
open_locale manifold
open finite_dimensional

local notation `E` n := euclidean_space ℝ (fin n)
local notation `𝕊` n := sphere (0 : (E n)) (1:ℝ)

instance two : fact (finrank ℝ (E 3) = 2 + 1) :=
sorry

instance three : fact (finrank ℝ (E 4) = 3 + 1) :=
sorry

lemma cont_diff_euclidean_rng_iff_pi {F ι : Type*} [normed_group F]
  [normed_space ℝ F] [fintype ι] {f : F → euclidean_space ℝ ι} {n : with_top ℕ} :
  cont_diff ℝ n f ↔ @cont_diff ℝ _ F _ _ (ι → ℝ) _ _ n (f : F → ι → ℝ) :=
let φ : euclidean_space ℝ ι ≃L[ℝ] ι → ℝ := (linear_equiv.refl ℝ _).to_continuous_linear_equiv in
⟨λ hf, φ.to_continuous_linear_map.cont_diff.comp hf,
 λ hf, φ.symm.to_continuous_linear_map.cont_diff.comp hf⟩

lemma cont_diff_euclidean_dom_iff_pi {F ι : Type*} [normed_group F]
  [normed_space ℝ F] [fintype ι] {f : euclidean_space ℝ ι → F} {n : with_top ℕ} :
  cont_diff ℝ n f ↔ @cont_diff ℝ _ (ι → ℝ) _ _ F _ _ n f :=
let φ : euclidean_space ℝ ι ≃L[ℝ] ι → ℝ := (linear_equiv.refl ℝ _).to_continuous_linear_equiv in
⟨λ hf, hf.comp φ.symm.to_continuous_linear_map.cont_diff,
 λ hf, hf.comp φ.to_continuous_linear_map.cont_diff⟩

lemma cont_diff_euclidean {F ι : Type*} [normed_group F]
  [normed_space ℝ F] [fintype ι] {f : F → euclidean_space ℝ ι} {n : with_top ℕ} :
  cont_diff ℝ n f ↔ ∀ i, cont_diff ℝ n (λ x, f x i) :=
by rw [cont_diff_euclidean_rng_iff_pi, cont_diff_pi]

/-
The relevant function from ℂ × ℂ to ℂ × ℝ is given by

 (z, w) ↦ (2 w* z, |z|^2 - |w|^2),

 i.e.

  (a + bi, c + di) ↦ (2 (ac + bd) + 2(bc-ad)i, a^2 + b^2 - (c^2 + d^2))

First, we express this as a function from ℝ^4 to ℝ^3.
-/
def hopf_fn (v : E 4) : E 3 :=
![ 2 * (v 0 * v 2 + v 1 * v 3), 2 * (v 1 * v 2 - v 0 * v 3),  (v 0)^2 + (v 1)^2 - (v 2)^2 - (v 3)^2]

/-
Then we show that it takes elements of S^3 maps to S^2.
We extract the relevant calculation for `polyrith`.
-/

theorem useful {v0 v1 v2 v3 : ℝ} (h : v0^2 + v1^2 + v2^2 + v3^2 = 1) :
  (2 * (v0 * v2 + v1 * v3))^2 + (2 * (v1 * v2 - v0 * v3))^2 + (v0^2 + v1^2 - v2^2 - v3^2)^2 = 1 :=
by { linear_combination (1 * v0 ^ 2 + 1 * v2 ^ 2 + 1 * v1 ^ 2 + 1 * v3 ^ 2 + 1) * h }


def hopf_map : (𝕊 4) → 𝕊 3 :=
set.cod_restrict (hopf_fn ∘ (coe : (𝕊 4) → E 4)) (𝕊 3)
begin
  intro v,
  have := v.property,
  simp [- norm_eq_of_mem_sphere, euclidean_space.norm_eq, finset.sum_fin_eq_sum_range, finset.sum_range_succ] at this,
  simp [hopf_fn, euclidean_space.norm_eq, finset.sum_fin_eq_sum_range, finset.sum_range_succ],
  rw if_pos, swap, norm_num,
  exact useful this
end

/-
We now show that the Hopf map from S^3 to S^2 is smooth
in the sense of smooth manifolds.
-/
theorem smooth_hopf_map : smooth (𝓡 3) (𝓡 2) hopf_map :=
begin
  apply cont_mdiff.cod_restrict_sphere,
  refine cont_mdiff.comp _ cont_mdiff_coe_sphere,
  rw cont_mdiff_iff_cont_diff,
  rw cont_diff_euclidean,
  intro i,
  fin_cases i;
  simp [hopf_fn];
  ring_nf;
  rw cont_diff_euclidean_dom_iff_pi,
  {
    apply_rules [cont_diff.add, cont_diff.mul, cont_diff_apply, cont_diff.neg, cont_diff_const],
  },
  {
    apply_rules [cont_diff.sub, cont_diff.mul, cont_diff_apply, cont_diff_const],
  },
  {
    apply_rules [cont_diff.add, cont_diff_apply, cont_diff.neg, cont_diff_const, cont_diff.pow],
  }
end

We now have smooth_hopf_map working! Taking a break for the day.

[Sam Freedman]

Tomorrow I'll be virtual, but I'll be following on Zulip if there's interest in doing coding sessions. Or I'll just bug people for possible next steps.

[Heather Macbeth]

@Sam Freedman Congrats!!

[Heather Macbeth]

@Sam Freedman I think the two stupid sorries are in the library as docs#fact_finite_dimensional_of_finrank_eq_succ

[Heather Macbeth]

Actually, that's not true, sorry. But here's some code for it:

lemma module.free.fact_finrank_pi_fin (R : Type*) [ring R] [strong_rank_condition R] (n : ℕ) :
  fact (finrank R (fin n → R) = n) :=
⟨begin
  rw module.free.finrank_pi R,
  exact fintype.card_fin n,
end⟩

lemma fact_finrank_euclidean (𝕜 : Type*) [is_R_or_C 𝕜] (n : ℕ) :
  fact (finrank 𝕜 (euclidean_space 𝕜 (fin n)) = n) :=
module.free.fact_finrank_pi_fin 𝕜 n

-- only in your file, it shouldn't be a global instance (we can discuss why)
local attribute [instance] fact_finrank_euclidean

[Anatole Dedecker]

(Just so that someone else doesn't start to work on it, I'm working on the PR about differentiability in docs#euclidean_space)

[Anatole Dedecker]

@Heather Macbeth On that note, do you think we should duplicate lemmas like the cont_diff_euclidean in the above code (which is a version of docs#cont_diff_pi), or should we just have the translation lemmas like cont_diff_euclidean_rng_iff_pi ?

[Heather Macbeth]

@Anatole Dedecker Actually, my instinct is to have cont_diff_euclidean but not cont_diff_euclidean_rng_iff_pi. I think people will always prefer to use that form.

[Anatole Dedecker]

Okay but then we need to duplicate a bunch of other thing. Just for the code above we also need a version of docs#cont_diff_apply

[Anatole Dedecker]

Well okay actually that might not be a bunch, this is somehow all you need to know it behaves like the product

[Anatole Dedecker]

So yeah I guess that works

[Anatole Dedecker]

(And yes, I also know you suggested to bypass docs#cont_diff_apply by invoking linearity, but we felt like invoking this directly was fine too)

[Heather Macbeth]

I was going to comment on that actually :)

[Anatole Dedecker]

Oh, sorry if I ruined the way you wanted to introduce things :sweat_smile:

[Heather Macbeth]

I think the principled way is to make a copy of linear_map.proj which uses Euclidean space as the domain rather than pi.

[Heather Macbeth]

Similar to how @Daniel Packer added docs#euclidean_space.single duplicating docs#pi.single.

[Sam Freedman]

Thanks @Heather Macbeth for the code, I’ll remove those sorry’s

[Sam Freedman]

@Heather Macbeth @Jeremy Avigad what do you think is the next place to go?
I think it would be cool to show it’s a fiber bundle. Or maybe we can show the fibers are circles? Not sure how to formalize this notion of isomorphism because the level sets p^-1(a) for a in S^2 and the circle S^1

[Heather Macbeth]

That's great! Maybe also surjectivity ...

[Heather Macbeth]

You said you were free until 11:45 today, but I'm not free til later unfortunately.

[Sam Freedman]

Heather Macbeth said:

You said you were free until 11:45 today, but I'm not free til later unfortunately.

Oh, I don’t have a restriction like that. What time is good to chat?

[Heather Macbeth]

Ah! Do you want to talk after the teaching discussion then?

[Sam Freedman]

I think touching base at 12:30 sounds good!

[Heather Macbeth]

@Sam Freedman The teaching session just ended, I can talk now if you're free but I will probably be at lunch at 12:30!

[Sam Freedman]

Talking now is great—do you have a Zoom link?

[Heather Macbeth]

PM'd you, others feel free to message me if you'd like to join.

[Jeremy Avigad]

Sorry I missed this... Busiso has been working on a calculation that shows that the fibers are circles in the simple case.

[Heather Macbeth]

Great! We arranged to meet again in person tomorrow to discuss next steps.

[Anatole Dedecker]

Here is the euclidean space differentiability PR : #15363