Complex manifolds: transport, quotients, bundles, and gluing

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremMöbius transformations of the projective line are analytic#

For 𝕜 = ℂ, every transformation z ↦ (a * z + b) / (c * z + d) of the Riemann sphere is holomorphic, and hence a biholomorphism Diffeomorph.constSmul 𝓘(ℂ) ω g with inverse the transformation of g⁻¹.

OnePoint.instContMDiffConstSMul.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜]
  [ProperSpace 𝕜] : ContMDiffConstSMul (modelWithCornersSelf 𝕜 𝕜) ⊤ (GL (Fin 2) 𝕜) (OnePoint 𝕜)

Lean

Formalized in Tau Ceti as OnePoint.instContMDiffConstSMul.

Sources

• Tau Ceti documentation: OnePoint.instContMDiffConstSMul
• Source of OnePoint.instContMDiffConstSMul in TauCeti/Geometry/Manifold/Instances/OnePoint/Moebius.lean
• Tau Ceti roadmap status: Complex manifolds: transport, quotients, bundles, and gluing

LeanOnePoint.instContMDiffConstSMul

TheoremTauCeti.contMDiff_orbitRelQuotientLift_iff#

For a free properly discontinuous action by C^n maps on a C^n manifold and m ≤ n, the descent of a G-invariant map is C^m exactly when the map is. For holomorphic actions on complex manifolds, this is the holomorphic descent of invariant holomorphic maps.

TauCeti.contMDiff_orbitRelQuotientLift_iff.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, u_8} {G : Type u_1}
  {M : Type u_2} {N : Type u_3} [Group G] [MulAction G M] [TopologicalSpace M] [TopologicalSpace N]
  {f : M → N} {hf : ∀ (g : G) (x : M), f (g • x) = f x} {𝕜 : Type u_4} [NontriviallyNormedField 𝕜]
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_6} [TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {E' : Type u_7} [NormedAddCommGroup E']
  [NormedSpace 𝕜 E'] {H' : Type u_8} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  [ChartedSpace H' N] {m n : WithTop ℕ∞} [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M]
  [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] [IsManifold I n M]
  [ContMDiffConstSMul I n G M] (hm : m ≤ n) :
  ContMDiff I I' m (TauCeti.MulAction.orbitRelQuotientLift f hf) ↔ ContMDiff I I' m f

Lean

Formalized in Tau Ceti as TauCeti.contMDiff_orbitRelQuotientLift_iff.

Sources

• Tau Ceti documentation: TauCeti.contMDiff_orbitRelQuotientLift_iff
• Source of TauCeti.contMDiff_orbitRelQuotientLift_iff in TauCeti/Geometry/Manifold/Quotient/Descent.lean
• Tau Ceti roadmap status: Complex manifolds: transport, quotients, bundles, and gluing

LeanTauCeti.contMDiff_orbitRelQuotientLift_iff

Uses 1

Statement usesDescent of an invariant map to the orbit space

TheoremTauCeti.contMDiff_orbitRelQuotientMap#

For free properly discontinuous actions by C^n maps on C^n manifolds and m ≤ n, a C^m map carrying one action to the other along σ induces a C^m map of orbit spaces.

TauCeti.contMDiff_orbitRelQuotientMap.{u_1, u_2, u_4, u_5, u_6, u_7, u_8, u_9, u_10} {G : Type u_1}
  {M : Type u_2} [Group G] [MulAction G M] [TopologicalSpace M] {𝕜 : Type u_4}
  [NontriviallyNormedField 𝕜] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_6}
  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {E' : Type u_7}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_8} [TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {m n : WithTop ℕ∞} [ProperlyDiscontinuousSMul G M]
  [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M]
  [IsManifold I n M] [ContMDiffConstSMul I n G M] {K : Type u_9} {N' : Type u_10} [Group K]
  [MulAction K N'] [TopologicalSpace N'] [ChartedSpace H' N'] [ProperlyDiscontinuousSMul K N']
  [ContinuousConstSMul K N'] [IsCancelSMul K N'] [T2Space N'] [LocallyCompactSpace N']
  [IsManifold I' n N'] [ContMDiffConstSMul I' n K N'] {σ : G → K} (hm : m ≤ n) {φ : M →ₑ[σ] N'}
  (hφ : ContMDiff I I' m ⇑φ) : ContMDiff I I' m φ.orbitRelQuotientMap

Lean

Formalized in Tau Ceti as TauCeti.contMDiff_orbitRelQuotientMap.

Sources

• Tau Ceti documentation: TauCeti.contMDiff_orbitRelQuotientMap
• Source of TauCeti.contMDiff_orbitRelQuotientMap in TauCeti/Geometry/Manifold/Quotient/Descent.lean
• Tau Ceti roadmap status: Complex manifolds: transport, quotients, bundles, and gluing

LeanTauCeti.contMDiff_orbitRelQuotientMap

Uses 1

Statement usesDescent of an invariant map to the orbit space

TheoremMDifferentiableAt.mfderiv_restrictScalars#

At a point where f is differentiable for the models over 𝕜', the derivative of f over the smaller field 𝕜 is its derivative over 𝕜' with scalars restricted to 𝕜, both read in the model spaces. For instance, the real derivative of a holomorphic map is its complex derivative.

MDifferentiableAt.mfderiv_restrictScalars.{u_1, u_2, u_3, u_4, u_5, u_6} (𝕜 : Type u_1)
  {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
  {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedSpace 𝕜' E']
  [IsScalarTower 𝕜 𝕜' E'] {M : Type u_5} [TopologicalSpace M] [ChartedSpace E M] {N : Type u_6}
  [TopologicalSpace N] [ChartedSpace E' N] {f : M → N} {x : M} (h : MDiffAt f x) :
  ↑(tangentSpaceCastModel (modelWithCornersSelf 𝕜 E') (f x)) ∘SL
      mfderiv% f x ∘SL ↑(tangentSpaceCastModel (modelWithCornersSelf 𝕜 E) x).symm =
    ContinuousLinearMap.restrictScalars 𝕜
      (↑(tangentSpaceCastModel (modelWithCornersSelf 𝕜' E') (f x)) ∘SL
        mfderiv% f x ∘SL ↑(tangentSpaceCastModel (modelWithCornersSelf 𝕜' E) x).symm)

Lean

Formalized in Tau Ceti as MDifferentiableAt.mfderiv_restrictScalars.

Sources

• Tau Ceti documentation: MDifferentiableAt.mfderiv_restrictScalars
• Source of MDifferentiableAt.mfderiv_restrictScalars in TauCeti/Geometry/Manifold/MFDeriv/RestrictScalars.lean
• Tau Ceti roadmap status: Complex manifolds: transport, quotients, bundles, and gluing

LeanMDifferentiableAt.mfderiv_restrictScalars

Used by 1

Used byAndreotti–Frankel theorem for proper holomorphic immersions

TheoremContMDiff.restrictScalars#

A C^n map for boundaryless models over 𝕜' is C^n for their scalar restrictions to 𝕜. For instance, a holomorphic map between complex manifolds is smooth.

ContMDiff.restrictScalars.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, u_8} (𝕜 : Type u_1) {𝕜' : Type u_2}
  [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {E' : Type u_4}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedSpace 𝕜' E'] [IsScalarTower 𝕜 𝕜' E']
  {H : Type u_5} {H' : Type u_6} [TopologicalSpace H] [TopologicalSpace H']
  {I : ModelWithCorners 𝕜' E H} {I' : ModelWithCorners 𝕜' E' H'} [I.Boundaryless] [I'.Boundaryless]
  {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N]
  [ChartedSpace H' N] {n : WithTop ℕ∞} {f : M → N} (h : ContMDiff I I' n f) :
  ContMDiff (ModelWithCorners.restrictScalars 𝕜 I) (ModelWithCorners.restrictScalars 𝕜 I') n f

Lean

Formalized in Tau Ceti as ContMDiff.restrictScalars.

Sources

• Tau Ceti documentation: ContMDiff.restrictScalars
• Source of ContMDiff.restrictScalars in TauCeti/Geometry/Manifold/ContMDiff/RestrictScalars.lean
• Tau Ceti roadmap status: Complex manifolds: transport, quotients, bundles, and gluing

LeanContMDiff.restrictScalars

Used by 2

Used byDiffeomorph.restrictScalars · Andreotti–Frankel theorem for proper holomorphic immersions

DefinitionHomeomorph.pullbackChartedSpace#

The charted-space structure on N pulled back along a homeomorphism e : N ≃ₜ M: the atlas is {e.transOpenPartialHomeomorph c | c ∈ atlas H M} and the chart at x is the chart of M at e x precomposed with e.

Homeomorph.pullbackChartedSpace.{u_1, u_2, u_3} {H : Type u_1} [TopologicalSpace H] {M : Type u_2}
  [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N] (e : N ≃ₜ M) :
  ChartedSpace H N

Lean

Formalized in Tau Ceti as Homeomorph.pullbackChartedSpace.

Sources

• Tau Ceti documentation: Homeomorph.pullbackChartedSpace
• Source of Homeomorph.pullbackChartedSpace in TauCeti/Geometry/Manifold/PullbackGroupoid.lean
• Tau Ceti roadmap status: Complex manifolds: transport, quotients, bundles, and gluing

LeanHomeomorph.pullbackChartedSpace

Used by 7

Used byThe boundary of a Liouville domain is of restricted contact type · Homeomorph.pullbackDiffeomorph · The regular-fibre theorem · The transverse fibre-product theorem · AddCircle.instIsManifold · AddCircle.isLocalDiffeomorph_coe · Volume-normalized total scalar curvature of a conformal metric

DefinitionHomeomorph.pullbackDiffeomorph#

A homeomorphism onto a charted space is a C^n diffeomorphism for the pulled-back structure: read in a pulled-back chart and in the corresponding chart of M, both it and its inverse are the identity.

Homeomorph.pullbackDiffeomorph.{u_1, u_2, u_3, u_5, u_6} {H : Type u_1} [TopologicalSpace H]
  {M : Type u_2} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_3} [TopologicalSpace N]
  {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] {E : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (e : N ≃ₜ M) : Diffeomorph I I N M n

Lean

Formalized in Tau Ceti as Homeomorph.pullbackDiffeomorph.

Sources

• Tau Ceti documentation: Homeomorph.pullbackDiffeomorph
• Source of Homeomorph.pullbackDiffeomorph in TauCeti/Geometry/Manifold/PullbackGroupoid.lean
• Tau Ceti roadmap status: Complex manifolds: transport, quotients, bundles, and gluing

LeanHomeomorph.pullbackDiffeomorph

Uses 1 · Used by 5

Statement usesHomeomorph.pullbackChartedSpace

Used byThe boundary of a Liouville domain is of restricted contact type · The regular-fibre theorem · The transverse fibre-product theorem · AddCircle.isLocalDiffeomorph_coe · Volume-normalized total scalar curvature of a conformal metric

DefinitionDiffeomorph.restrictScalars#

A C^n diffeomorphism for boundaryless models over 𝕜' is a C^n diffeomorphism for their scalar restrictions to 𝕜, with the same underlying equivalence. For instance, a biholomorphism between complex manifolds is a diffeomorphism of the underlying real manifolds.

Diffeomorph.restrictScalars.{u_1, u_2, u_3, u_4, u_6, u_7, u_9, u_10} (𝕜 : Type u_1) {𝕜' : Type u_2}
  [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {E' : Type u_4}
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedSpace 𝕜' E'] [IsScalarTower 𝕜 𝕜' E']
  {H : Type u_6} {H' : Type u_7} [TopologicalSpace H] [TopologicalSpace H']
  {I : ModelWithCorners 𝕜' E H} {I' : ModelWithCorners 𝕜' E' H'} [I.Boundaryless] [I'.Boundaryless]
  {M : Type u_9} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_10} [TopologicalSpace N]
  [ChartedSpace H' N] {n : WithTop ℕ∞} (Φ : Diffeomorph I I' M N n) :
  Diffeomorph (ModelWithCorners.restrictScalars 𝕜 I) (ModelWithCorners.restrictScalars 𝕜 I') M N n

Lean

Formalized in Tau Ceti as Diffeomorph.restrictScalars.

Sources

• Tau Ceti documentation: Diffeomorph.restrictScalars
• Source of Diffeomorph.restrictScalars in TauCeti/Geometry/Manifold/Diffeomorph/RestrictScalars.lean
• Tau Ceti roadmap status: Complex manifolds: transport, quotients, bundles, and gluing

LeanDiffeomorph.restrictScalars

Uses 1

Proof usesContMDiff.restrictScalars

DefinitionDescent of an invariant map to the orbit space#

A map f : X → Y that is invariant under the action of G factors through the orbit projection X → MulAction.orbitRel.Quotient G X.

TauCeti.MulAction.orbitRelQuotientLift.{u_1, u_2, u_3} {G : Type u_1} {X : Type u_2} [Group G]
  [MulAction G X] {Y : Type u_3} (f : X → Y) (hf : ∀ (g : G) (x : X), f (g • x) = f x) :
  MulAction.orbitRel.Quotient G X → Y

Lean

Formalized in Tau Ceti as TauCeti.MulAction.orbitRelQuotientLift.

Sources

• Tau Ceti documentation: TauCeti.MulAction.orbitRelQuotientLift
• Source of TauCeti.MulAction.orbitRelQuotientLift in TauCeti/Algebra/GroupAction/OrbitRelQuotient.lean
• Tau Ceti roadmap status: Complex manifolds: transport, quotients, bundles, and gluing

LeanTauCeti.MulAction.orbitRelQuotientLift

Used by 5

Used byTauCeti.ModularGroup.jBiholomorph · The degree of a finite-index map of compactified Fuchsian quotients is the index · The uniformization theorem · TauCeti.contMDiff_orbitRelQuotientLift_iff · TauCeti.contMDiff_orbitRelQuotientMap

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.