Documentation

LeanPool.JacobianDiffgeo.ProjectiveLine.Charts

The two-chart complex-manifold structure on ℙ¹ (CC5) #

Unit: projective-line (docs/design/projective-line.md §3.2). Builds ChartedSpace ℂ (OnePoint ℂ) and IsManifold 𝓘(ℂ) ω (OnePoint ℂ) from two charts:

coeChart is hand-rolled (not built from isOpenEmbedding_coe.toOpenPartialHomeomorph) so that coeChart ∞ = 0 is rfl; invChart is likewise hand-rolled (toFun p := coeChart (inversion p), invFun w := inversion ↑w) so that all four transition maps between coeChart/invChart are literally id/Inv.inv as total functions (junk values aligned by construction).

source
noncomputable def RS.P1.coeChart :
OpenPartialHomeomorph (OnePoint ℂ) ℂ

The identity chart on the finite part of ℙ¹: source {∞}ᶜ, target univ, ↑z ↦ z, junk value coeChart ∞ = 0.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem RS.P1.coeChart_apply_coe (z : ℂ) :
    ↑coeChart ↑z = z
    source
    @[simp]
    theorem RS.P1.coeChart_apply_infty :
    ↑coeChart OnePoint.infty = 0
    source
    @[simp]
    theorem RS.P1.coeChart_symm_apply (z : ℂ) :
    ↑coeChart.symm z = ↑z
    source
    @[simp]
    theorem RS.P1.coeChart_source :
    coeChart.source = {OnePoint.infty}ᶜ
    source
    @[simp]
    theorem RS.P1.coeChart_target :
    coeChart.target = Set.univ
    source
    theorem RS.P1.inversion_coe_ne_coe_zero (w : ℂ) :
    inversion ↑w ≠ ↑0

    inversion never sends a finite point to ↑(0:ℂ).

    source
    noncomputable def RS.P1.invChart :
    OpenPartialHomeomorph (OnePoint ℂ) ℂ

    The chart at infinity: source {(0:ℂ)}ᶜ, target univ, ↑z ↦ z⁻¹, ∞ ↦ 0. Hand-rolled (toFun p := coeChart (inversion p), invFun w := inversion ↑w), matching coeChart's style so junk values are aligned.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem RS.P1.invChart_apply_coe (z : ℂ) :
      ↑invChart ↑z = z⁻¹
      source
      @[simp]
      theorem RS.P1.invChart_apply_infty :
      ↑invChart OnePoint.infty = 0
      source
      @[simp]
      theorem RS.P1.invChart_symm_apply (w : ℂ) :
      ↑invChart.symm w = inversion ↑w
      source
      @[simp]
      theorem RS.P1.invChart_source :
      invChart.source = {↑0}ᶜ
      source
      @[simp]
      theorem RS.P1.invChart_target :
      invChart.target = Set.univ
      source
      theorem RS.P1.invChart_comp_coe :
      ↑invChart ∘ OnePoint.some = Inv.inv
      source
      theorem RS.P1.coeChart_inversion_coe (z : ℂ) :
      ↑coeChart (inversion ↑z) = z⁻¹

      inversion read through coeChart on both ends is inversion itself (unconditional).

      source
      theorem RS.P1.invChart_inversion_coe (z : ℂ) :
      ↑invChart (inversion ↑z) = z

      inversion read through invChart on both ends is the identity (unconditional; this is invChart.right_inv unfolded through invChart_symm_apply).

      source
      noncomputable def RS.P1.chartFamily :
      Bool → OpenPartialHomeomorph (OnePoint ℂ) ℂ

      The generating chart family (false ↦ coeChart, true ↦ invChart).

      Equations
      Instances For
        source
        @[simp]
        theorem RS.P1.chartFamily_false :
        chartFamily false = coeChart
        source
        @[simp]
        theorem RS.P1.chartFamily_true :
        chartFamily true = invChart
        source
        def RS.P1.chartIndex :
        OnePoint ℂ → Bool

        Index map: ∞ ↦ true (use invChart), ↑z ↦ false (use coeChart).

        Equations
        Instances For
          source
          @[simp]
          theorem RS.P1.chartIndex_infty :
          chartIndex OnePoint.infty = true
          source
          @[simp]
          theorem RS.P1.chartIndex_coe (z : ℂ) :
          chartIndex ↑z = false
          source
          theorem RS.P1.mem_chartFamily_source (p : OnePoint ℂ) :
          p ∈ (chartFamily (chartIndex p)).source
          source
          @[instance_reducible]
          noncomputable instance RS.P1.instChartedSpace :
          ChartedSpace ℂ (OnePoint ℂ)
          Equations
          source
          @[simp]
          theorem RS.P1.chartAt_coe (z : ℂ) :
          chartAt ℂ ↑z = coeChart
          source
          @[simp]
          theorem RS.P1.chartAt_infty :
          chartAt ℂ OnePoint.infty = invChart
          source
          theorem RS.P1.atlas_eq :
          atlas ℂ (OnePoint ℂ) = {coeChart, invChart}
          source
          instance RS.P1.instIsManifold :
          IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ (OnePoint ℂ)
          source
          theorem RS.P1.coeChart_mem_maximalAtlas :
          coeChart ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ (OnePoint ℂ)
          source
          theorem RS.P1.invChart_mem_maximalAtlas :
          invChart ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ (OnePoint ℂ)
          source
          instance RS.P1.instNontrivialOnePointComplex_leanPool :
          Nontrivial (OnePoint ℂ)

          Classical.arbitrary-free basepoints: ∞, ↑0, ↑1.