The curvature of the geometric phase is the Fubini–Study form

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #65 and #89, the residues of #54 (brick BP-3 of specs/berry-phase-scoping.md).

GeometricPhaseCurvature.lean proves the curvature formula β = −∫∫ 2 Im⟪∂_sΨ, ∂_tΨ⟫ for a C² family of unit vectors, and says in its honest scope that identifying that integrand with the corpus's Fubini–Study form is open. This module closes it:

2 Im⟪∂_sΨ, ∂_tΨ⟫ = −(1/2) · ω_FS on the velocities of the projected family [Ψ],

so β = (1/2) ∫∫ [Ψ]^* ω_FS — Berry's phase as the integral of the Kähler form over the disc.

The route

• ★ studyForm ψ u v = Im⟪u,v⟫/‖ψ‖² − Im(⟪u,ψ⟫⟪ψ,v⟫)/‖ψ‖⁴ — the Fubini–Study form written on homogeneous coordinates, the Im twin of FisherRao.fsInnerHom. Its two properties are the whole geometry: ★★ studyForm_lift — it does not change when the lift is rescaled by a scalar and the velocities are changed by multiples of the lift (ψ ↦ cψ, u ↦ cu + aψ), which is exactly the freedom in choosing a lift of a curve of rays; and ★ studyForm_of_unit — for a unit lift it is plainly Im⟪u,v⟫, because the correction term is real (the fibre direction is imaginary).
• ★★ fsModelForm_eq_studyForm — the model form at w is −4 studyForm of the lifts insertOne i w, insertZero i u (the form twin of fsMetric_eq_fsInnerHom).
• chartVelCLM i v — the differential of the affine chart on representatives, and ★ hasFDerivAt_coordRatio: the chart coordinates of a differentiable family of lifts are differentiable, with that velocity. insertZero_chartVelCLM expresses the lifted chart velocity as a • v + (v i)⁻¹ • d, which is what studyForm_lift consumes, giving ★★ studyForm_chartVelCLM — the chart form on the chart velocities is the homogeneous form on the original lift and its velocities.
• ★★★ fsModelForm_eq_neg_two_mul_curvature (chart level, any chart containing the point) and ★★★ fsForm_eq_neg_two_mul_curvature (the form of ProjectiveSpaceFubiniStudyForm.lean at the ray [Ψ p], in the atlas's own chart) — the curvature is −1/2 of the Fubini–Study form on the velocities of the projected family.
• ★★ hasMFDerivAt_projFamily — those velocities are the pushforward: the manifold derivative of q ↦ [Ψ q] is the derivative of the chart path, for a family indexed by any normed space (F = ℝ is the curve hasMFDerivAt_projCurve, F = ℝ × ℝ the two-parameter map of the rectangle), so the two theorems above are the pullback [Ψ]^* ω_FS and not merely a formula in a chart.
• ★★★ geometricPhase_eq_half_integral_fsPullback — the curvature formula of #54 restated: β = (1/2) ∫₀¹ ∫₀ᵀ [Ψ]^* ω_FS.

The pullback as a form (#89)

The theorems above pair ω_FS with the two coordinate directions, so fsPullback is a function of the parameter. The pullback is a form:

• ★ fsPullbackForm Ψ h p — [Ψ]^* ω_FS at p: the form of ℂℙⁿ at [Ψ p] composed with mfderiv, so alternation is structural and not a proved identity;
• ★★★ fsPullbackForm_apply — the chart-free formula [Ψ]^* ω_FS (a, b) = −4 studyForm (Ψ p) (∂_aΨ) (∂_bΨ), for every nonvanishing differentiable family, unit or not. Every trace of the atlas's chart choice idx [Ψ p] is gone, which is what fsPullbackForm_eq_chart (the same form in any chart containing the ray) and the smoothness argument need;
• ★★ contDiffAt_fsPullbackForm and ★★★ fsPullbackDifferentialForm — a bundled C^∞ 2-form on the parameter space, a term of DifferentialForm 𝓘(ℝ, F) F ∞ (Fin 2) ℝ; on the rectangle F = ℝ × ℝ this is [Ψ]^* ω_FS as a differential form on the disc's parameter domain. The local representative is the section itself, because a normed space is its own chart (instHasTranslationAtlasSelf, added to TranslationAtlasForm.lean);
• ★★ fsPullbackForm_apply_coord — the form on the coordinate directions is fsPullback, so ★★★ curvature_eq_neg_half_fsPullbackForm and ★★★ geometricPhase_eq_half_integral_fsPullbackForm restate #65's two theorems with the form as a form. The quotient rule the chart path needs is HasFDerivAt.div, which Analysis/Calculus/FDeriv/Quotient.lean supplies because Mathlib has no such lemma at the pin (MATHLIB-ABSENT(HasFDerivAt.div), checked there).

The normalisation

None is chosen here: fsForm is the dd^c form of log(1 + ‖z‖²) (fsChartForm), whose value at a chart origin is −4 times Im⟪·,·⟫ (fsChartForm_zero), and the −1/2 above is what that convention forces. The check is BP-2: on ℂℙ¹ the cone's disc gives β = −Ω/2 for the solid angle Ω (Empirical/QM/BerryPhaseCurvature.lean), and fsForm has total mass 4π on ℂℙ¹ (fsVolume_eq_smul_fsMeasure), the solid angle of the whole sphere.

Honest scope

⚠️ The disc is a rectangle, as in #54: this is Green's theorem in a chart, not Stokes on a manifold. What is proved here is the integrand — the pointwise identification of the curvature with ω_FS on the pushed-forward velocities — and the integral in geometricPhase_eq_half_integral_fsPullback is the iterated interval integral of that function, which is the same number as ∫∫ [Ψ]^* ω_FS would be. The corpus integrates a top-degree form as a measure (topFormMeasure, riemannianVolume); integration of a 2-form over a 2-chain is not defined here and is not claimed.

⚠️ fsPullbackDifferentialForm is built for this family directly, out of the chart-free formula fsPullbackForm_apply; it is not an instance of a general “pullback of a differential form along a smooth map”, which the corpus does not define. Nothing here integrates the form as a form either: geometricPhase_eq_half_integral_fsPullbackForm is the iterated interval integral of its value on the coordinate directions, by the paragraph above.

References: M. V. Berry, Proc. R. Soc. A 392 (1984) 45, §3; B. Simon, PRL 51 (1983) 2167; Y. Aharonov, J. Anandan, PRL 58 (1987) 1593; specs/berry-phase-scoping.md BP-3; specs/BACKLOG.md #65, #89; specs/future-work.md.

The Fubini–Study form on homogeneous coordinates

noncomputable def Projectivization.studyForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (ψ u v : E) : ℝ

The Fubini–Study form written on homogeneous coordinates: for a lift ψ ≠ 0 and velocities u, v, studyForm ψ u v = Im⟪u,v⟫/‖ψ‖² − Im(⟪u,ψ⟫⟪ψ,v⟫)/‖ψ‖⁴. This is the Im twin of FisherRao.fsInnerHom, the Fubini–Study metric in the same coordinates.

Equations

• Projectivization.studyForm ψ u v = (inner ℂ u v).im / ‖ψ‖ ^ 2 - (inner ℂ u ψ * inner ℂ ψ v).im / ‖ψ‖ ^ 4

theorem Projectivization.studyForm_add_smul_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : E} (hψ : ψ ≠ 0) (u v : E) (a : ℂ) : studyForm ψ (u + a • ψ) v = studyForm ψ u v

Adding a multiple of the lift to the first velocity does not change the form: the fibre direction is in the kernel.

theorem Projectivization.studyForm_add_smul_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : E} (hψ : ψ ≠ 0) (u v : E) (b : ℂ) : studyForm ψ u (v + b • ψ) = studyForm ψ u v

Adding a multiple of the lift to the second velocity does not change the form.

theorem Projectivization.studyForm_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : E} (hψ : ψ ≠ 0) {c : ℂ} (hc : c ≠ 0) (u v : E) : studyForm (c • ψ) (c • u) (c • v) = studyForm ψ u v

Rescaling the lift and the velocities together does not change the form.

theorem Projectivization.studyForm_lift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ : E} (hψ : ψ ≠ 0) {c : ℂ} (hc : c ≠ 0) (u v : E) (a b : ℂ) : studyForm (c • ψ) (c • u + a • ψ) (c • v + b • ψ) = studyForm ψ u v

★★ The form depends only on the curve of rays. Rescaling the lift by c ≠ 0 and changing the velocities by arbitrary multiples of the lift — which is exactly the freedom in lifting a curve of rays — leaves studyForm unchanged.

theorem Projectivization.studyForm_of_unit {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ψ u v : E} (h1 : ‖ψ‖ = 1) (hu : (inner ℂ ψ u).re = 0) (hv : (inner ℂ ψ v).re = 0) : studyForm ψ u v = (inner ℂ u v).im

★ For a unit lift the form is plainly Im⟪u,v⟫: the correction term is real, because ⟪ψ, u⟫ and ⟪ψ, v⟫ are purely imaginary along a family of unit vectors.

theorem Projectivization.re_inner_deriv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {γ : ℝ → E} {D : E} {x : ℝ} (hγ : HasDerivAt γ D x) (hunit : ∀ (y : ℝ), ‖γ y‖ = 1) : (inner ℂ (γ x) D).re = 0

Along a family of unit vectors the inner product of the value with the velocity is purely imaginary: differentiating ‖γ‖² = 1.

The model form on the lifts

theorem Projectivization.fsModelForm_eq_studyForm {n : ℕ} (i : Fin (n + 1)) (w u v : Fin n → ℂ) : (fsModelForm w) ![u, v] = -4 * studyForm (insertOne i w) (insertZero i u) (insertZero i v)

★★ The model form is −4 times the homogeneous form on the lifts — the Im twin of fsMetric_eq_fsInnerHom: the Fubini–Study form of the i-th affine chart at w, evaluated on chart directions u, v, is studyForm of the lifts insertOne i w, insertZero i u, insertZero i v.

The differential of the affine chart, on representatives

noncomputable def Projectivization.chartVelCLM {n : ℕ} (i : Fin (n + 1)) (v : Ambient n) : Ambient n →L[ℂ] Fin n → ℂ

The differential of coordRatio i at v: the velocity of the affine chart coordinates, a ℂ-linear map of the velocity of the representative.

Equations

• One or more equations did not get rendered due to their size.

theorem Projectivization.chartVelCLM_apply {n : ℕ} (i : Fin (n + 1)) (v d : Ambient n) (j : Fin n) : (chartVelCLM i v) d j = (d.ofLp (i.succAbove j) * v.ofLp i - v.ofLp (i.succAbove j) * d.ofLp i) / v.ofLp i ^ 2

theorem Projectivization.hasFDerivAt_coordRatio {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ψ : F → Ambient n} {D : F →L[ℝ] Ambient n} {p : F} (hΨ : HasFDerivAt Ψ D p) (i : Fin (n + 1)) (hi : (Ψ p).ofLp i ≠ 0) : HasFDerivAt (fun (q : F) => coordRatio i (Ψ q)) (ContinuousLinearMap.restrictScalars ℝ (chartVelCLM i (Ψ p)) ∘SL D) p

★ The chart coordinates of a differentiable family of representatives are differentiable, with velocity chartVelCLM composed with the family's derivative: the quotient rule (HasFDerivAt.div, the lemma Analysis/Calculus/FDeriv/Quotient.lean adds) coordinate by coordinate, for a family indexed by any normed space — the two-parameter case is F = ℝ × ℝ.

theorem Projectivization.hasDerivAt_coordRatio {n : ℕ} {γ : ℝ → Ambient n} {D : Ambient n} {x : ℝ} (hγ : HasDerivAt γ D x) (i : Fin (n + 1)) (hi : (γ x).ofLp i ≠ 0) : HasDerivAt (fun (y : ℝ) => coordRatio i (γ y)) ((chartVelCLM i (γ x)) D) x

★ The chart coordinates of a differentiable curve of representatives are differentiable, with velocity chartVelCLM: the curve case of hasFDerivAt_coordRatio.

The lifted chart velocity

theorem Projectivization.insertOne_coordRatio {n : ℕ} (i : Fin (n + 1)) {v : Ambient n} (hv : v.ofLp i ≠ 0) : insertOne i (coordRatio i v) = (v.ofLp i)⁻¹ • v

The affine section applied to the chart coordinates rescales the representative.

theorem Projectivization.insertZero_chartVelCLM {n : ℕ} (i : Fin (n + 1)) {v : Ambient n} (hv : v.ofLp i ≠ 0) (d : Ambient n) : insertZero i ((chartVelCLM i v) d) = (-d.ofLp i / v.ofLp i ^ 2) • v + (v.ofLp i)⁻¹ • d

★ The lifted chart velocity is the velocity of the rescaled representative: the lift of chartVelCLM i v d differs from (v i)⁻¹ • d by a multiple of v — which is exactly the freedom studyForm_lift absorbs.

theorem Projectivization.studyForm_chartVelCLM {n : ℕ} (i : Fin (n + 1)) {v : Ambient n} (hv0 : v ≠ 0) (hvi : v.ofLp i ≠ 0) (d e : Ambient n) : studyForm (insertOne i (coordRatio i v)) (insertZero i ((chartVelCLM i v) d)) (insertZero i ((chartVelCLM i v) e)) = studyForm v d e

★★ The chart form on the chart velocities is the homogeneous form on the representative. Every trace of the chart is gone from the right-hand side: this is where the projective invariance of studyForm is spent.

The curvature is the Fubini–Study form

theorem Projectivization.hasDerivAt_edgeS {n : ℕ} {Ψ : ℝ × ℝ → Ambient n} {s t : ℝ} (hΨ : DifferentiableAt ℝ Ψ (s, t)) : HasDerivAt (fun (s : ℝ) => Ψ (s, t)) ((fderiv ℝ Ψ (s, t)) (1, 0)) s

The s-edge of a family, as a curve with the partial derivative as its velocity.

theorem Projectivization.hasDerivAt_edgeT {n : ℕ} {Ψ : ℝ × ℝ → Ambient n} {s t : ℝ} (hΨ : DifferentiableAt ℝ Ψ (s, t)) : HasDerivAt (fun (t : ℝ) => Ψ (s, t)) ((fderiv ℝ Ψ (s, t)) (0, 1)) t

The t-edge of a family, as a curve with the partial derivative as its velocity.

theorem Projectivization.ne_zero_of_norm_eq_one {n : ℕ} {v : Ambient n} (h : ‖v‖ = 1) : v ≠ 0

theorem Projectivization.fsModelForm_eq_neg_two_mul_curvature {n : ℕ} {Ψ : ℝ × ℝ → Ambient n} {s t : ℝ} (hΨ : DifferentiableAt ℝ Ψ (s, t)) (hunit : ∀ (q : ℝ × ℝ), ‖Ψ q‖ = 1) (i : Fin (n + 1)) (hi : (Ψ (s, t)).ofLp i ≠ 0) : (fsModelForm (coordRatio i (Ψ (s, t)))) ![deriv (fun (s : ℝ) => coordRatio i (Ψ (s, t))) s, deriv (fun (t : ℝ) => coordRatio i (Ψ (s, t))) t] = -2 * GeometricPhase.curvature Ψ (s, t)

★★★ The curvature of the geometric phase is the Fubini–Study form, in any affine chart containing the ray: for a family of unit vectors differentiable at (s, t), the chart form at the chart point, evaluated on the velocities of the chart path, is −2 times the curvature 2 Im⟪∂_sΨ, ∂_tΨ⟫.

The projected family

noncomputable def Projectivization.projFamily {n : ℕ} {ι : Type u_1} (Ψ : ι → Ambient n) (h : ∀ (q : ι), Ψ q ≠ 0) (q : ι) : Projectivization ℂ (Ambient n)

The projection of a family of nonzero representatives to ℂℙⁿ.

Equations

• Projectivization.projFamily Ψ h q = Projectivization.mk ℂ (Ψ q) ⋯

theorem Projectivization.idx_ne_zero {n : ℕ} {ι : Type u_1} {Ψ : ι → Ambient n} (h : ∀ (q : ι), Ψ q ≠ 0) (q : ι) : (Ψ q).ofLp (projFamily Ψ h q).idx ≠ 0

The atlas's chart at the projected point contains it: the representative's coordinate there does not vanish.

theorem Projectivization.hasMFDerivAt_projCurve {n : ℕ} {γ : ℝ → Ambient n} (h : ∀ (y : ℝ), γ y ≠ 0) {D : Ambient n} {x : ℝ} (hγ : HasDerivAt γ D x) : HasMFDerivAt% (projFamily γ h) x (ContinuousLinearMap.smulRight 1 ((chartVelCLM (projFamily γ h x).idx (γ x)) D))

★★ The chart velocity is the pushforward. The manifold derivative of the projected curve y ↦ [γ y] is the derivative of its chart path, so the tangent vectors of fsForm_eq_neg_two_mul_curvature are the pushforwards of the coordinate directions and the identification is the pullback [Ψ]^* ω_FS.

theorem Projectivization.fsForm_eq_neg_two_mul_curvature {n : ℕ} {Ψ : ℝ × ℝ → Ambient n} (h : ∀ (q : ℝ × ℝ), Ψ q ≠ 0) (hunit : ∀ (q : ℝ × ℝ), ‖Ψ q‖ = 1) {s t : ℝ} (hΨ : DifferentiableAt ℝ Ψ (s, t)) : (fsForm (projFamily Ψ h (s, t))) ![deriv (fun (a : ℝ) => coordRatio (projFamily Ψ h (s, t)).idx (Ψ (a, t))) s, deriv (fun (b : ℝ) => coordRatio (projFamily Ψ h (s, t)).idx (Ψ (s, b))) t] = -2 * GeometricPhase.curvature Ψ (s, t)

★★★ The curvature is −1/2 of the Fubini–Study form of ℂℙⁿ on the velocities of the projected family, in the atlas's own chart at the point — the identification the honest scope of GeometricPhaseCurvature.lean left open.

The curvature formula as an integral of the Fubini–Study form

noncomputable def Projectivization.fsPullback {n : ℕ} (Ψ : ℝ × ℝ → Ambient n) (h : ∀ (q : ℝ × ℝ), Ψ q ≠ 0) (p : ℝ × ℝ) : ℝ

The pullback of the Fubini–Study form along the projected family, on the coordinate directions: ([Ψ])^* ω_FS (∂_s, ∂_t).

Equations

• One or more equations did not get rendered due to their size.

theorem Projectivization.curvature_eq_neg_half_fsPullback {n : ℕ} {Ψ : ℝ × ℝ → Ambient n} (h : ∀ (q : ℝ × ℝ), Ψ q ≠ 0) (hunit : ∀ (q : ℝ × ℝ), ‖Ψ q‖ = 1) {s t : ℝ} (hΨ : DifferentiableAt ℝ Ψ (s, t)) : GeometricPhase.curvature Ψ (s, t) = -(1 / 2) * fsPullback Ψ h (s, t)

★★★ The pointwise identification, in the form the integral consumes.

theorem Projectivization.geometricPhase_eq_half_integral_fsPullback {n : ℕ} {Ψ : ℝ × ℝ → Ambient n} (h : ∀ (q : ℝ × ℝ), Ψ q ≠ 0) (hΨ : ContDiff ℝ 2 Ψ) (hunit : ∀ (p : ℝ × ℝ), ‖Ψ p‖ = 1) {T : ℝ} {φ : ℝ → ℝ} (hφ : ContDiff ℝ 1 φ) (hφ0 : φ 0 = 0) (hleft : ∀ (t : ℝ), Ψ (0, t) = Ψ (0, 0)) (htop : ∀ (s : ℝ), Ψ (s, T) = Complex.exp (↑(φ s) * Complex.I) • Ψ (s, 0)) : GeometricPhase.geometricPhase (fun (t : ℝ) => Ψ (1, t)) T (φ 1) = 1 / 2 * ∫ (s : ℝ) in 0..1, ∫ (t : ℝ) in 0..T, fsPullback Ψ h (s, t)

★★★ Berry's phase is half the integral of the Fubini–Study form over the disc. The curvature formula of GeometricPhaseCurvature.lean with its integrand identified: for a C² family of unit vectors on [0,1] × [0,T] — the disc in polar form, the inner edge collapsed, the cut carrying the total phase φ 1 — the geometric phase of the loop is (1/2) ∫∫ [Ψ]^* ω_FS.

The two-parameter pushforward, and the pullback as a form

theorem Projectivization.hasMFDerivAt_projFamily {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ψ : F → Ambient n} (h : ∀ (q : F), Ψ q ≠ 0) {D : F →L[ℝ] Ambient n} {p : F} (hΨ : HasFDerivAt Ψ D p) : HasMFDerivAt% (projFamily Ψ h) p (ContinuousLinearMap.restrictScalars ℝ (chartVelCLM (projFamily Ψ h p).idx (Ψ p)) ∘SL D)

★★ The chart velocity is the pushforward, for a family indexed by any normed space. The manifold derivative of q ↦ [Ψ q] is the derivative of its chart path; with F = ℝ × ℝ this is the two-parameter map of fsForm_eq_neg_two_mul_curvature, so that identification is the pullback [Ψ]^* ω_FS and not merely a formula in a chart.

theorem Projectivization.mfderiv_projFamily_apply {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ψ : F → Ambient n} (h : ∀ (q : F), Ψ q ≠ 0) {p : F} (hΨ : DifferentiableAt ℝ Ψ p) (a : F) : (mfderiv% (projFamily Ψ h) p) a = (chartVelCLM (projFamily Ψ h p).idx (Ψ p)) ((fderiv ℝ Ψ p) a)

The pushforward of a coordinate direction is the derivative of the chart path along it — for F = ℝ × ℝ and the direction (1, 0), exactly the derivative fsPullback is written with.

noncomputable def Projectivization.fsPullbackForm {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (Ψ : F → Ambient n) (h : ∀ (q : F), Ψ q ≠ 0) (p : F) : F [⋀^Fin 2]→L[ℝ] ℝ

★ The pullback of the Fubini–Study form along a projected family, [Ψ]^* ω_FS, as an alternating 2-form at each parameter: the form of ℂℙⁿ at [Ψ p] composed with the manifold derivative of q ↦ [Ψ q]. Alternation is now structural rather than a proved identity.

Equations

• Projectivization.fsPullbackForm Ψ h p = (Projectivization.fsForm (Projectivization.projFamily Ψ h p)).compContinuousLinearMap (mfderiv% (Projectivization.projFamily Ψ h) p)

theorem Projectivization.fsPullbackForm_apply {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ψ : F → Ambient n} (h : ∀ (q : F), Ψ q ≠ 0) {D : F →L[ℝ] Ambient n} {p : F} (hΨ : HasFDerivAt Ψ D p) (a b : F) : (fsPullbackForm Ψ h p) ![a, b] = -4 * studyForm (Ψ p) (D a) (D b)

★★★ The pullback on a pair of directions is the homogeneous form on the lift and its velocities — no chart anywhere on the right-hand side: [Ψ]^* ω_FS (a, b) = −4 studyForm (Ψ p) (∂_a Ψ) (∂_b Ψ). This is fsModelForm_eq_studyForm and studyForm_chartVelCLM read through the pushforward, and it holds for every nonvanishing differentiable family, unit or not.

theorem Projectivization.fsPullbackForm_eq_chart {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ψ : F → Ambient n} (h : ∀ (q : F), Ψ q ≠ 0) {q : F} (hdiff : DifferentiableAt ℝ Ψ q) (i : Fin (n + 1)) (hi : (Ψ q).ofLp i ≠ 0) : fsPullbackForm Ψ h q = (fsModelForm (coordRatio i (Ψ q))).compContinuousLinearMap (fderiv ℝ (fun (y : F) => coordRatio i (Ψ y)) q)

In any affine chart containing the ray, the pullback is the model form on the chart path's derivative. The atlas's own choice idx [Ψ p] jumps as p moves; this says the pullback does not, which is what makes it smooth.

theorem Projectivization.contDiffAt_coordRatio {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ψ : F → Ambient n} (hΨ : ContDiff ℝ (↑⊤) Ψ) (i : Fin (n + 1)) {q : F} (hq : (Ψ q).ofLp i ≠ 0) : ContDiffAt ℝ (↑⊤) (fun (y : F) => coordRatio i (Ψ y)) q

The chart path of a C^∞ family is C^∞ where the chart is defined.

theorem Projectivization.contDiffAt_fsPullbackForm {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ψ : F → Ambient n} (h : ∀ (q : F), Ψ q ≠ 0) (hΨ : ContDiff ℝ (↑⊤) Ψ) (p : F) : ContDiffAt ℝ (↑⊤) (fun (q : F) => fsPullbackForm Ψ h q) p

★★ The pullback is a C^∞ family of forms. In a fixed chart it is the model form on the chart path's derivative (fsPullbackForm_eq_chart), the model form is C^∞ (contDiff_fsModelForm), the derivative of a C^∞ map is C^∞, and the pullback operation is jointly smooth in the form and the linear map (ContinuousAlternatingMap.contDiff_uncurry_compContinuousLinearMap).

noncomputable def Projectivization.fsPullbackFamily {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (Ψ : F → Ambient n) (h : ∀ (q : F), Ψ q ≠ 0) (p : F) : TangentSpace (modelWithCornersSelf ℝ F) p [⋀^Fin 2]→L[ℝ] Bundle.Trivial F ℝ p

The pullback read in the fibres of the alternating bundle over the parameter space.

Equations

• Projectivization.fsPullbackFamily Ψ h p = Projectivization.fsPullbackForm Ψ h p

theorem Projectivization.contMDiff_fsPullbackFamily {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ψ : F → Ambient n} (h : ∀ (q : F), Ψ q ≠ 0) (hΨ : ContDiff ℝ (↑⊤) Ψ) : ContMDiff (modelWithCornersSelf ℝ F) ((modelWithCornersSelf ℝ F).prod (modelWithCornersSelf ℝ (F [⋀^Fin 2]→L[ℝ] ℝ))) ↑⊤ fun (p : F) => ⟨p, fsPullbackFamily Ψ h p⟩

The pullback is a C^∞ section: the parameter space is its own chart, so its local representative is itself (HasTranslationAtlas), and that is contDiffAt_fsPullbackForm.

noncomputable def Projectivization.fsPullbackDifferentialForm {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (Ψ : F → Ambient n) (h : ∀ (q : F), Ψ q ≠ 0) (hΨ : ContDiff ℝ (↑⊤) Ψ) : DifferentialForm (modelWithCornersSelf ℝ F) F (↑⊤) (Fin 2) ℝ

★★★ [Ψ]^* ω_FS as a differential 2-form on the parameter space — for F = ℝ × ℝ, on the rectangle of GeometricPhaseCurvature.lean: a bundled C^∞ section of the alternating-2-form bundle, not a function of the two coordinate directions.

Equations

• Projectivization.fsPullbackDifferentialForm Ψ h hΨ = { toFun := Projectivization.fsPullbackFamily Ψ h, contMDiff_toFun := ⋯ }

@[simp]

theorem Projectivization.fsPullbackDifferentialForm_apply {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (Ψ : F → Ambient n) (h : ∀ (q : F), Ψ q ≠ 0) (hΨ : ContDiff ℝ (↑⊤) Ψ) (p : F) (v : Fin 2 → F) : ((fsPullbackDifferentialForm Ψ h hΨ) p) v = (fsPullbackForm Ψ h p) v

The form and the curvature formula

theorem Projectivization.fsPullbackForm_apply_coord {n : ℕ} {Ψ : ℝ × ℝ → Ambient n} (h : ∀ (q : ℝ × ℝ), Ψ q ≠ 0) {p : ℝ × ℝ} (hΨ : DifferentiableAt ℝ Ψ p) : (fsPullbackForm Ψ h p) ![(1, 0), (0, 1)] = fsPullback Ψ h p

★★ The form on the coordinate directions is the function of fsPullback — the two readings of [Ψ]^* ω_FS agree.

theorem Projectivization.curvature_eq_neg_half_fsPullbackForm {n : ℕ} {Ψ : ℝ × ℝ → Ambient n} (h : ∀ (q : ℝ × ℝ), Ψ q ≠ 0) (hunit : ∀ (q : ℝ × ℝ), ‖Ψ q‖ = 1) {p : ℝ × ℝ} (hΨ : DifferentiableAt ℝ Ψ p) : GeometricPhase.curvature Ψ p = -(1 / 2) * (fsPullbackForm Ψ h p) ![(1, 0), (0, 1)]

★★★ The curvature is −1/2 of the Fubini–Study form, with the form now a form: the pullback 2-form of the projected family, evaluated on the two coordinate directions of the rectangle.

theorem Projectivization.geometricPhase_eq_half_integral_fsPullbackForm {n : ℕ} {Ψ : ℝ × ℝ → Ambient n} (h : ∀ (q : ℝ × ℝ), Ψ q ≠ 0) (hΨ : ContDiff ℝ 2 Ψ) (hunit : ∀ (p : ℝ × ℝ), ‖Ψ p‖ = 1) {T : ℝ} {φ : ℝ → ℝ} (hφ : ContDiff ℝ 1 φ) (hφ0 : φ 0 = 0) (hleft : ∀ (t : ℝ), Ψ (0, t) = Ψ (0, 0)) (htop : ∀ (s : ℝ), Ψ (s, T) = Complex.exp (↑(φ s) * Complex.I) • Ψ (s, 0)) : GeometricPhase.geometricPhase (fun (t : ℝ) => Ψ (1, t)) T (φ 1) = 1 / 2 * ∫ (s : ℝ) in 0..1, ∫ (t : ℝ) in 0..T, (fsPullbackForm Ψ h (s, t)) ![(1, 0), (0, 1)]

★★★ Berry's phase is half the integral of the pullback form. geometricPhase_eq_half_integral_fsPullback with its integrand read as [Ψ]^* ω_FS paired with the coordinate directions.