The (p,q) type of complex-valued alternating forms

Let J be a continuous real-linear endomorphism of a real topological vector space V with J² = -1, and let F be a complex topological vector space. A continuous real alternating map ω : V [⋀^Fin k]→L[ℝ] F is a complex-valued k-form on V, and it decomposes uniquely into components of type (p,q), p + q = k. This file develops that decomposition directly on the real alternating carrier, without passing to the complexification of V.

Every endomorphism J of V acts on forms as a derivation, J.alternatingDerivation ω v = ∑ i, ω (update v i (J (v i))). On a form of type (p,q) it acts by (p - q) * I, and since p + q = k this eigenvalue determines (p,q); this is the definition of ContinuousAlternatingMap.IsOfType. A one-form α has type (1,0) exactly when α (J v) = I • α v, and type (0,1) exactly when α (J v) = -I • α v.

When J² = -1, every polynomial vanishing at the numbers (p - q) * I with p + q = k annihilates the derivation on k-forms. Since these numbers are distinct, the corresponding Lagrange basis polynomials, evaluated at the derivation, are the type projections ContinuousLinearMap.typeProjection J p q. They are complementary idempotents whose ranges are the forms of each type. Types and type projections are compatible with pullback along maps intertwining the complex structures and with complex-linear coefficient maps, and conjugate-linear coefficient maps such as complex conjugation exchange the types (p,q) and (q,p).

These fibrewise statements are the linear algebra behind the type decomposition of complex-valued differential forms on an almost complex manifold.

Main declarations

• ContinuousLinearMap.alternatingDerivation: an endomorphism of V acting as a derivation on alternating maps.
• ContinuousLinearMap.alternatingDerivation_alternatingDerivation_sub: the commutator of two derivations is the derivation of the commutator.
• ContinuousAlternatingMap.IsOfType: a k-form has type (p,q).
• ContinuousAlternatingMap.IsOfType.alternatingDerivation_alternatingDerivation_of_anticomm: the derivation of an endomorphism anticommuting with J shifts the type of a form.
• ContinuousLinearMap.aeval_alternatingDerivation_eq_zero: the polynomial identity satisfied by the derivation of an endomorphism with J² = -1.
• ContinuousLinearMap.typeProjection: for J² = -1, the projection onto the forms of type (p,q).
• ContinuousLinearMap.typePolynomial, ContinuousLinearMap.typeProjection_eq_aeval: the polynomial, independent of J, whose value at the derivation is the type projection.
• ContinuousLinearMap.sum_typeProjection: a form is the sum of its components of each type.
• ContinuousLinearMap.typeProjection_alternatingDerivation: the type projections commute with the derivation.
• ContinuousLinearMap.isOfType_typeProjection, ContinuousAlternatingMap.IsOfType.typeProjection_self: the projections land in, and fix, the forms of their type.
• ContinuousLinearMap.typeProjection_eq_of_sum_eq: uniqueness of the type decomposition.
• ContinuousAlternatingMap.isOfType_one_zero_iff, ContinuousAlternatingMap.isOfType_zero_one_iff, ContinuousLinearMap.typeProjection_one_zero and ContinuousLinearMap.typeProjection_zero_one: one-forms.
• ContinuousAlternatingMap.IsOfType.map_smul_complex and ContinuousAlternatingMap.IsOfType.map_smul_conj: on a complex vector space, one-forms of type (1,0) are complex-linear and one-forms of type (0,1) are conjugate-linear.
• ContinuousLinearMap.typeProjection_two_zero_apply, ContinuousLinearMap.typeProjection_one_one_apply and ContinuousLinearMap.typeProjection_zero_two_apply: the type components of two-forms, in terms of the values of the form with J applied to its arguments.

Implementation notes

The polynomial identity is proved by induction on the degree. Inserting a vector v as the first argument, the combinations ι_v ∓ I • ι_{J v} of interior products (ContinuousAlternatingMap.curryLeftTopologicalLinear) intertwine the derivation on (k+1)-forms with the derivation on k-forms shifted by ±I.

References

• Daniel Huybrechts, Complex Geometry: An Introduction, Universitext, Springer, 2005, Section 1.2.

def ContinuousLinearMap.alternatingDerivation {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (J : V →L[ℝ] V) : V [⋀^ι]→L[ℝ] F →ₗ[ℂ] V [⋀^ι]→L[ℝ] F

An endomorphism J of V acts on alternating maps on V as a derivation: the result is the sum, over all arguments, of the alternating map with J applied to that argument.

theorem ContinuousLinearMap.alternatingDerivation_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (J : V →L[ℝ] V) (ω : V [⋀^ι]→L[ℝ] F) (v : ι → V) : (J.alternatingDerivation ω) v = ∑ i : ι, ω (Function.update v i (J (v i)))

@[simp]

theorem ContinuousLinearMap.toAlternatingMap_alternatingDerivation {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (J : V →L[ℝ] V) (ω : V [⋀^ι]→L[ℝ] F) : (J.alternatingDerivation ω).toAlternatingMap = (↑J).alternatingDerivation ω.toAlternatingMap

The continuous derivation is the derivation LinearMap.alternatingDerivation of the underlying linear endomorphism on the underlying alternating maps.

theorem ContinuousLinearMap.alternatingDerivation_apply_vecCons_fin_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] (J : V →L[ℝ] V) (α : V [⋀^Fin 1]→L[ℝ] F) (v : V) : (J.alternatingDerivation α) ![v] = α ![J v]

On a one-form, the derivation is precomposition with J.

theorem ContinuousLinearMap.alternatingDerivation_apply_vecCons_fin_two {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] (J : V →L[ℝ] V) (β : V [⋀^Fin 2]→L[ℝ] F) (v w : V) : (J.alternatingDerivation β) ![v, w] = β ![J v, w] + β ![v, J w]

On a two-form, the derivation applies J to each argument in turn.

theorem ContinuousLinearMap.alternatingDerivation_compContinuousLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] [AddCommGroup W] [Module ℝ W] [TopologicalSpace W] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {J : V →L[ℝ] V} {K : W →L[ℝ] W} {f : W →L[ℝ] V} (hf : ∀ (w : W), J (f w) = f (K w)) (ω : V [⋀^ι]→L[ℝ] F) : K.alternatingDerivation (ω.compContinuousLinearMap f) = (J.alternatingDerivation ω).compContinuousLinearMap f

The derivation is natural for pullback along a map intertwining the endomorphisms.

theorem ContinuousLinearMap.alternatingDerivation_compContinuousAlternatingMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} {G : Type u_4} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] [AddCommGroup G] [Module ℂ G] [Module ℝ G] [IsScalarTower ℝ ℂ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul ℂ G] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (J : V →L[ℝ] V) (L : F →L[ℝ] G) (ω : V [⋀^ι]→L[ℝ] F) : J.alternatingDerivation (L.compContinuousAlternatingMap ω) = L.compContinuousAlternatingMap (J.alternatingDerivation ω)

The derivation commutes with real-linear coefficient maps.

theorem ContinuousLinearMap.alternatingDerivation_alternatingDerivation_sub {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (J B : V →L[ℝ] V) (ω : V [⋀^ι]→L[ℝ] F) : J.alternatingDerivation (B.alternatingDerivation ω) - B.alternatingDerivation (J.alternatingDerivation ω) = (B ∘SL J).alternatingDerivation ω - (J ∘SL B).alternatingDerivation ω

The commutator of the derivations induced by two endomorphisms is induced by their commutator, taken in the opposite order since the endomorphisms act on the arguments of a form.

def ContinuousAlternatingMap.IsOfType {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} (ω : V [⋀^Fin k]→L[ℝ] F) (J : V →L[ℝ] V) (p q : ℕ) : Prop

A complex-valued k-form ω has type (p,q) for J when p + q = k and the derivation induced by J acts on ω as multiplication by (p - q) * I. For an almost complex structure J, these are the forms whose complex-multilinear extension to the complexification vanishes unless exactly p of its arguments are of type (1,0) and the other q of type (0,1).

theorem ContinuousAlternatingMap.isOfType_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} : ω.IsOfType J p q ↔ p + q = k ∧ J.alternatingDerivation ω = ((↑p - ↑q) * Complex.I) • ω

theorem ContinuousAlternatingMap.IsOfType.add_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} (h : ω.IsOfType J p q) : p + q = k

theorem ContinuousAlternatingMap.IsOfType.alternatingDerivation_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} (h : ω.IsOfType J p q) : J.alternatingDerivation ω = ((↑p - ↑q) * Complex.I) • ω

theorem ContinuousAlternatingMap.IsOfType.alternatingDerivation_alternatingDerivation_of_anticomm {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} {X : V →L[ℝ] V} (hω : ω.IsOfType J p q) (hX : ∀ (w : V), X (J w) = -J (X w)) : J.alternatingDerivation (X.alternatingDerivation ω) = ((↑p - ↑q) * Complex.I) • X.alternatingDerivation ω + 2 • (X ∘SL J).alternatingDerivation ω

For a form ω of type (p,q) and an endomorphism X anticommuting with J, the derivation of J acts on X.alternatingDerivation ω as (p - q) * I up to twice the derivation of X ∘ J. Since X ∘ J also anticommutes with J, this is why X moves the type by (±1,∓1).

@[simp]

theorem ContinuousAlternatingMap.isOfType_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {p q : ℕ} : IsOfType 0 J p q ↔ p + q = k

theorem ContinuousAlternatingMap.IsOfType.add {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {ω ω' : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} (h : ω.IsOfType J p q) (h' : ω'.IsOfType J p q) : (ω + ω').IsOfType J p q

theorem ContinuousAlternatingMap.IsOfType.smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} (h : ω.IsOfType J p q) (c : ℂ) : (c • ω).IsOfType J p q

theorem ContinuousAlternatingMap.IsOfType.neg {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} (h : ω.IsOfType J p q) : (-ω).IsOfType J p q

theorem ContinuousAlternatingMap.IsOfType.sub {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {ω ω' : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} (h : ω.IsOfType J p q) (h' : ω'.IsOfType J p q) : (ω - ω').IsOfType J p q

theorem ContinuousAlternatingMap.isOfType_zero_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] (ω : V [⋀^Fin 0]→L[ℝ] F) (J : V →L[ℝ] V) : ω.IsOfType J 0 0

Every complex-valued function, as a 0-form, has type (0,0).

theorem ContinuousAlternatingMap.isOfType_one_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} (α : V [⋀^Fin 1]→L[ℝ] F) : α.IsOfType J 1 0 ↔ ∀ (v : V), α ![J v] = Complex.I • α ![v]

A one-form has type (1,0) exactly when it is complex-linear for J.

theorem ContinuousAlternatingMap.isOfType_zero_one_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} (α : V [⋀^Fin 1]→L[ℝ] F) : α.IsOfType J 0 1 ↔ ∀ (v : V), α ![J v] = -Complex.I • α ![v]

A one-form has type (0,1) exactly when it is conjugate-linear for J.

theorem ContinuousAlternatingMap.IsOfType.map_smul_complex {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {U : Type u_5} [AddCommGroup U] [Module ℂ U] [Module ℝ U] [IsScalarTower ℝ ℂ U] [TopologicalSpace U] [ContinuousConstSMul ℂ U] {α : U [⋀^Fin 1]→L[ℝ] F} (h : α.IsOfType (Complex.I • ContinuousLinearMap.id ℝ U) 1 0) (c : ℂ) (v : U) : α ![c • v] = c • α ![v]

On a complex vector space, a one-form of type (1,0) for multiplication by i is complex-linear.

theorem ContinuousAlternatingMap.IsOfType.map_smul_conj {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {U : Type u_5} [AddCommGroup U] [Module ℂ U] [Module ℝ U] [IsScalarTower ℝ ℂ U] [TopologicalSpace U] [ContinuousConstSMul ℂ U] {α : U [⋀^Fin 1]→L[ℝ] F} (h : α.IsOfType (Complex.I • ContinuousLinearMap.id ℝ U) 0 1) (c : ℂ) (v : U) : α ![c • v] = (starRingEnd ℂ) c • α ![v]

On a complex vector space, a one-form of type (0,1) for multiplication by i is conjugate-linear.

theorem ContinuousAlternatingMap.IsOfType.apply_eq_sum_conj_smul {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {α : (ι → ℂ) [⋀^Fin 1]→L[ℝ] F} (h : α.IsOfType (Complex.I • ContinuousLinearMap.id ℝ (ι → ℂ)) 0 1) (v : ι → ℂ) : α ![v] = ∑ i : ι, (starRingEnd ℂ) (v i) • α ![Pi.single i 1]

A one-form of type (0,1) on a finite complex coordinate space is the sum of its coordinate values, weighted by the conjugates of the vector coordinates.

theorem ContinuousAlternatingMap.IsOfType.eq_zero_of_apply_eq_zero {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {U : Type u_5} [AddCommGroup U] [Module ℂ U] [Module ℝ U] [IsScalarTower ℝ ℂ U] [TopologicalSpace U] [ContinuousConstSMul ℂ U] {α : U [⋀^Fin 1]→L[ℝ] F} (h : α.IsOfType (Complex.I • ContinuousLinearMap.id ℝ U) 1 0) (hU : Module.finrank ℂ U = 1) {w : U} (hw : w ≠ 0) (hα : α ![w] = 0) : α = 0

On a one-dimensional complex vector space, a one-form of type (1,0) for multiplication by i which vanishes on a nonzero vector is zero.

theorem ContinuousAlternatingMap.IsOfType.compContinuousLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] [AddCommGroup W] [Module ℝ W] [TopologicalSpace W] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} {J : V →L[ℝ] V} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} {K : W →L[ℝ] W} {f : W →L[ℝ] V} (hf : ∀ (w : W), J (f w) = f (K w)) (h : ω.IsOfType J p q) : (ω.compContinuousLinearMap f).IsOfType K p q

Pullback along a map intertwining the endomorphisms preserves type.

theorem ContinuousAlternatingMap.IsOfType.compContinuousAlternatingMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} {G : Type u_4} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] [AddCommGroup G] [Module ℂ G] [Module ℝ G] [IsScalarTower ℝ ℂ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul ℂ G] {k : ℕ} {J : V →L[ℝ] V} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} {L : F →L[ℝ] G} (hL : ∀ (c : ℂ) (x : F), L (c • x) = c • L x) (h : ω.IsOfType J p q) : (L.compContinuousAlternatingMap ω).IsOfType J p q

A complex-linear coefficient map preserves type.

theorem ContinuousAlternatingMap.IsOfType.compContinuousAlternatingMap_of_map_smul_conj {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} {G : Type u_4} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] [AddCommGroup G] [Module ℂ G] [Module ℝ G] [IsScalarTower ℝ ℂ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul ℂ G] {k : ℕ} {J : V →L[ℝ] V} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} {L : F →L[ℝ] G} (hL : ∀ (c : ℂ) (x : F), L (c • x) = (starRingEnd ℂ) c • L x) (h : ω.IsOfType J p q) : (L.compContinuousAlternatingMap ω).IsOfType J q p

A conjugate-linear coefficient map, such as complex conjugation, exchanges the types (p,q) and (q,p).

noncomputable def ContinuousLinearMap.typeProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] (J : V →L[ℝ] V) {k : ℕ} (p q : ℕ) : Module.End ℂ (V [⋀^Fin k]→L[ℝ] F)

The Lagrange basis polynomial at (p - q) * I of the nodes (p' - q') * I, p' + q' = k, evaluated at the derivation induced by J on complex-valued k-forms. For J² = -1 this is the projection onto the forms of type (p,q) for J, and it vanishes unless p + q = k.

noncomputable def ContinuousLinearMap.typePolynomial (k p q : ℕ) : Polynomial ℂ

The polynomial defining the type projections: the Lagrange basis polynomial at (p - q) * I of the nodes (p' - q') * I, p' + q' = k. It does not depend on J, so the type projections of any endomorphism are this polynomial evaluated at its derivation.

theorem ContinuousLinearMap.typeProjection_eq_aeval {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] (J : V →L[ℝ] V) {k : ℕ} (p q : ℕ) : J.typeProjection p q = (Polynomial.aeval J.alternatingDerivation) (typePolynomial k p q)

The type projection is the type polynomial evaluated at the derivation.

theorem ContinuousLinearMap.sum_typeProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {k : ℕ} (J : V →L[ℝ] V) (ω : V [⋀^Fin k]→L[ℝ] F) : ∑ pq ∈ Finset.antidiagonal k, (J.typeProjection pq.1 pq.2) ω = ω

The operators J.typeProjection p q with p + q = k sum to the identity on k-forms. For J² = -1, this says that every complex-valued form is the sum of its components of each type.

@[simp]

theorem ContinuousAlternatingMap.IsOfType.typeProjection_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} (h : ω.IsOfType J p q) : (J.typeProjection p q) ω = ω

The projection onto type (p,q) fixes the forms of type (p,q).

theorem ContinuousAlternatingMap.IsOfType.typeProjection_of_ne {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} {ω : V [⋀^Fin k]→L[ℝ] F} {p q p' q' : ℕ} (h : ω.IsOfType J p q) (hne : (p', q') ≠ (p, q)) : (J.typeProjection p' q') ω = 0

The projection onto any other type annihilates the forms of type (p,q).

theorem ContinuousAlternatingMap.IsOfType.eq_zero_of_ne {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} {ω : V [⋀^Fin k]→L[ℝ] F} {p q p' q' : ℕ} (h : ω.IsOfType J p q) (h' : ω.IsOfType J p' q') (hne : (p, q) ≠ (p', q')) : ω = 0

A form of two different types vanishes.

theorem ContinuousLinearMap.typeProjection_eq_of_sum_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} {η : ℕ × ℕ → V [⋀^Fin k]→L[ℝ] F} (hη : ∀ pq ∈ Finset.antidiagonal k, (η pq).IsOfType J pq.1 pq.2) (hω : ∑ pq ∈ Finset.antidiagonal k, η pq = ω) (hpq : p + q = k) : (J.typeProjection p q) ω = η (p, q)

The components of a sum of forms of each type are its type components.

theorem ContinuousLinearMap.typeProjection_one_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] (J : V →L[ℝ] V) : J.typeProjection 1 0 = 2⁻¹ • (1 - Complex.I • J.alternatingDerivation)

On one-forms, J.typeProjection 1 0 sends α to (α - I • α ∘ J) / 2. For J² = -1, this is the type-(1,0) component of α.

theorem ContinuousLinearMap.typeProjection_zero_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] (J : V →L[ℝ] V) : J.typeProjection 0 1 = 2⁻¹ • (1 + Complex.I • J.alternatingDerivation)

On one-forms, J.typeProjection 0 1 sends α to (α + I • α ∘ J) / 2. For J² = -1, this is the type-(0,1) component of α.

theorem ContinuousLinearMap.alternatingDerivation_alternatingDerivation_apply_vecCons_fin_two {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} (hJ : ∀ (v : V), J (J v) = -v) (β : V [⋀^Fin 2]→L[ℝ] F) (v w : V) : (J.alternatingDerivation (J.alternatingDerivation β)) ![v, w] = 2 • (β ![J v, J w] - β ![v, w])

On two-forms, for J² = -1, the square of the derivation sends β to 2 • (β ∘ (J × J) - β).

theorem ContinuousLinearMap.typeProjection_two_zero_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} (hJ : ∀ (v : V), J (J v) = -v) (β : V [⋀^Fin 2]→L[ℝ] F) (v w : V) : ((J.typeProjection 2 0) β) ![v, w] = 4⁻¹ • (β ![v, w] - β ![J v, J w] - Complex.I • (β ![J v, w] + β ![v, J w]))

On two-forms, for J² = -1, the type-(2,0) component of β is (β - β ∘ (J × J) - I • (β (J ·, ·) + β (·, J ·))) / 4.

theorem ContinuousLinearMap.typeProjection_one_one_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} (hJ : ∀ (v : V), J (J v) = -v) (β : V [⋀^Fin 2]→L[ℝ] F) (v w : V) : ((J.typeProjection 1 1) β) ![v, w] = 2⁻¹ • (β ![v, w] + β ![J v, J w])

On two-forms, for J² = -1, the type-(1,1) component of β is (β + β ∘ (J × J)) / 2.

theorem ContinuousLinearMap.typeProjection_zero_two_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} (hJ : ∀ (v : V), J (J v) = -v) (β : V [⋀^Fin 2]→L[ℝ] F) (v w : V) : ((J.typeProjection 0 2) β) ![v, w] = 4⁻¹ • (β ![v, w] - β ![J v, J w] + Complex.I • (β ![J v, w] + β ![v, J w]))

On two-forms, for J² = -1, the type-(0,2) component of β is (β - β ∘ (J × J) + I • (β (J ·, ·) + β (·, J ·))) / 4.

theorem ContinuousLinearMap.typeProjection_compContinuousLinearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] [AddCommGroup W] [Module ℝ W] [TopologicalSpace W] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k p q : ℕ} {K : W →L[ℝ] W} {f : W →L[ℝ] V} (hf : ∀ (w : W), J (f w) = f (K w)) (ω : V [⋀^Fin k]→L[ℝ] F) : (K.typeProjection p q) (ω.compContinuousLinearMap f) = ((J.typeProjection p q) ω).compContinuousLinearMap f

Pullback along a map intertwining the endomorphisms commutes with the type projections.

theorem ContinuousLinearMap.typeProjection_compContinuousAlternatingMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} {G : Type u_4} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] [AddCommGroup G] [Module ℂ G] [Module ℝ G] [IsScalarTower ℝ ℂ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul ℂ G] {J : V →L[ℝ] V} {k p q : ℕ} {L : F →L[ℝ] G} (hL : ∀ (c : ℂ) (x : F), L (c • x) = c • L x) (ω : V [⋀^Fin k]→L[ℝ] F) : (J.typeProjection p q) (L.compContinuousAlternatingMap ω) = L.compContinuousAlternatingMap ((J.typeProjection p q) ω)

A complex-linear coefficient map commutes with the type projections.

theorem ContinuousLinearMap.typeProjection_compContinuousAlternatingMap_of_map_smul_conj {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} {G : Type u_4} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] [AddCommGroup G] [Module ℂ G] [Module ℝ G] [IsScalarTower ℝ ℂ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul ℂ G] {J : V →L[ℝ] V} {k p q : ℕ} {L : F →L[ℝ] G} (hL : ∀ (c : ℂ) (x : F), L (c • x) = (starRingEnd ℂ) c • L x) (ω : V [⋀^Fin k]→L[ℝ] F) : (J.typeProjection q p) (L.compContinuousAlternatingMap ω) = L.compContinuousAlternatingMap ((J.typeProjection p q) ω)

A conjugate-linear coefficient map, such as complex conjugation, sends the type-(p,q) projection to the type-(q,p) projection.

theorem ContinuousLinearMap.aeval_alternatingDerivation_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} [ContinuousConstSMul ℝ F] (hJ : ∀ (v : V), J (J v) = -v) {g : Polynomial ℂ} (hg : ∀ (p q : ℕ), p + q = k → Polynomial.eval ((↑p - ↑q) * Complex.I) g = 0) : (Polynomial.aeval J.alternatingDerivation) g = 0

For J² = -1, a polynomial vanishing at every eigenvalue (p - q) * I with p + q = k annihilates the derivation induced by J on complex-valued k-forms.

theorem ContinuousLinearMap.alternatingDerivation_typeProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} [ContinuousConstSMul ℝ F] {p q : ℕ} (hJ : ∀ (v : V), J (J v) = -v) (ω : V [⋀^Fin k]→L[ℝ] F) : J.alternatingDerivation ((J.typeProjection p q) ω) = ((↑p - ↑q) * Complex.I) • (J.typeProjection p q) ω

The derivation acts on the type-(p,q) component by (p - q) * I.

theorem ContinuousLinearMap.typeProjection_alternatingDerivation {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} [ContinuousConstSMul ℝ F] {p q : ℕ} (hJ : ∀ (v : V), J (J v) = -v) (ω : V [⋀^Fin k]→L[ℝ] F) : (J.typeProjection p q) (J.alternatingDerivation ω) = ((↑p - ↑q) * Complex.I) • (J.typeProjection p q) ω

The derivation of J and the type projections commute, so the type-(p,q) projection turns the derivation into multiplication by (p - q) * I.

theorem ContinuousLinearMap.isOfType_typeProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} [ContinuousConstSMul ℝ F] {p q : ℕ} (hJ : ∀ (v : V), J (J v) = -v) (hpq : p + q = k) (ω : V [⋀^Fin k]→L[ℝ] F) : ((J.typeProjection p q) ω).IsOfType J p q

The type-(p,q) component of a form has type (p,q).

@[simp]

theorem ContinuousLinearMap.typeProjection_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} [ContinuousConstSMul ℝ F] {p q : ℕ} (hJ : ∀ (v : V), J (J v) = -v) (hpq : p + q ≠ k) : J.typeProjection p q = 0

The type-(p,q) projection of k-forms vanishes unless p + q = k.

theorem ContinuousLinearMap.isOfType_iff_typeProjection_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} [ContinuousConstSMul ℝ F] {ω : V [⋀^Fin k]→L[ℝ] F} {p q : ℕ} (hJ : ∀ (v : V), J (J v) = -v) : ω.IsOfType J p q ↔ p + q = k ∧ (J.typeProjection p q) ω = ω

A form has type (p,q) exactly when p + q = k and its type-(p,q) component is the whole form.

@[simp]

theorem ContinuousLinearMap.typeProjection_typeProjection {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] {F : Type u_3} [AddCommGroup F] [Module ℂ F] [Module ℝ F] [IsScalarTower ℝ ℂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul ℂ F] {J : V →L[ℝ] V} {k : ℕ} [ContinuousConstSMul ℝ F] {p q p' q' : ℕ} (hJ : ∀ (v : V), J (J v) = -v) (ω : V [⋀^Fin k]→L[ℝ] F) : (J.typeProjection p' q') ((J.typeProjection p q) ω) = if (p', q') = (p, q) then (J.typeProjection p q) ω else 0

The type projections are complementary idempotents.