Coefficient maps and coefficient scalars of differential forms #
A continuous real-linear map L : F →L[ℝ] G of coefficient spaces sends an F-valued
differential form to the G-valued form RoughForm.mapCoeff L φ, obtained by applying L to
each value. This preserves regularity, commutes with pullback, and commutes with the exterior
derivative of differentiable forms. On smooth forms it is the real-linear map
SmoothForm.mapCoeff L.
Scalars acting on the coefficients act on smooth forms through the coefficient map given by
multiplication by the scalar. When F is a complex vector space, this makes
SmoothForm I M F k a complex vector space whose complex scalars restrict to its existing real
scalars, as needed for complex-valued forms on complex manifolds, and the exterior derivative
and pullback are complex-linear. The scalar action is defined on underlying forms pointwise,
so for real scalars it agrees with the submodule action on SmoothForm I M F k up to reducible
unfolding of instances. Coefficient conjugation of complex-valued forms is conjugate-linear.
The paired wedge is natural for coefficient maps intertwining two pairings. A pairing that turns multiplication by one scalar into multiplication by another makes the wedge of smooth forms semilinear in the same way; in particular, the wedge for a complex-bilinear pairing of complex coefficient spaces is complex-linear in each form. Coefficient conjugation is multiplicative for the wedge of complex-valued forms given by complex multiplication.
Main declarations #
TauCeti.RoughForm.mapCoeff,TauCeti.SmoothForm.mapCoeff: coefficient maps of forms.TauCeti.IsSmoothForm.mapCoeff: coefficient maps preserve regularity.TauCeti.mextDerivWithin_mapCoeff,TauCeti.mextDeriv_mapCoeff: naturality of the exterior derivative in the coefficient space.TauCeti.mpullbackWithin_mapCoeff,TauCeti.mpullback_mapCoeff: coefficient maps commute with pullback.TauCeti.SmoothForm.instModule: the action of scalars on the coefficients, for instance complex scalars on complex-valued forms, withTauCeti.SmoothForm.smul_toRoughFormandTauCeti.SmoothForm.smul_eq_mapCoeff.TauCeti.SmoothForm.mextDerivₗ_smul,TauCeti.SmoothForm.mpullback_smul: the exterior derivative and pullback are linear for these scalars.TauCeti.SmoothForm.mapCoeff_conj_smul: coefficient conjugation is conjugate-linear.TauCeti.RoughForm.mapCoeff_wedgeWith,TauCeti.SmoothForm.mapCoeff_wedgeWith: naturality of the paired wedge in the coefficients.TauCeti.SmoothForm.wedgeWith_smul_left_of_map_smul,TauCeti.SmoothForm.wedgeWith_smul_right_of_map_smul: the paired wedge is linear, or semilinear, for scalars acting on the coefficients compatibly with the pairing.TauCeti.SmoothForm.mapCoeff_conj_wedgeWith_mul: coefficient conjugation of the wedge of complex-valued forms.
References #
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Chapter 14.
Coefficient maps of rough forms #
noncomputable def
TauCeti.RoughForm.mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(L : F →L[ℝ] G)
(φ : RoughForm I M F k)
:
RoughForm I M G k
The form obtained by applying a fixed continuous linear map of coefficient spaces to the values of a form.
Instances For
@[simp]
theorem
TauCeti.RoughForm.mapCoeff_apply
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(L : F →L[ℝ] G)
(φ : RoughForm I M F k)
(x : M)
(v : Fin k → TangentSpace I x)
:
@[simp]
theorem
TauCeti.RoughForm.mapCoeff_zero
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(L : F →L[ℝ] G)
:
@[simp]
theorem
TauCeti.RoughForm.mapCoeff_add
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(L : F →L[ℝ] G)
(φ ψ : RoughForm I M F k)
:
@[simp]
theorem
TauCeti.RoughForm.mapCoeff_smul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(L : F →L[ℝ] G)
(c : ℝ)
(φ : RoughForm I M F k)
:
@[simp]
theorem
TauCeti.RoughForm.mapCoeff_id
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
(φ : RoughForm I M F k)
:
@[simp]
theorem
TauCeti.RoughForm.mapCoeff_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
{G' : Type u_9}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup G']
[NormedSpace ℝ G']
{k : ℕ}
(L' : G →L[ℝ] G')
(L : F →L[ℝ] G)
(φ : RoughForm I M F k)
:
theorem
TauCeti.RoughForm.smul_eq_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
{S : Type u_10}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
(c : S)
(φ : RoughForm I M F k)
:
Scalar multiplication of the coefficients is the coefficient map given by multiplication by the scalar.
theorem
TauCeti.RoughForm.mapCoeff_smul_of_map_smul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{S : Type u_10}
{S' : Type u_11}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
[Monoid S']
[DistribMulAction S' G]
[ContinuousConstSMul S' G]
[SMulCommClass ℝ S' G]
(L : F →L[ℝ] G)
{c : S}
{d : S'}
(hL : ∀ (v : F), L (c • v) = d • L v)
(φ : RoughForm I M F k)
:
A coefficient map that is semilinear for scalars c ↦ d turns multiplication by c into
multiplication by d.
theorem
TauCeti.RoughForm.inChartAt_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(L : F →L[ℝ] G)
(φ : RoughForm I M F k)
(x₀ : M)
:
In every chart, the coordinate expression of a coefficient map of a form is the coefficient map of its coordinate expression.
theorem
TauCeti.IsSmoothForm.mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
[IsManifold I 1 M]
{n : WithTop ℕ∞}
{φ : RoughForm I M F k}
(hφ : IsSmoothForm I n φ)
(L : F →L[ℝ] G)
:
IsSmoothForm I n (RoughForm.mapCoeff L φ)
A coefficient map preserves the regularity of a form.
theorem
TauCeti.mextDerivWithin_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(L : F →L[ℝ] G)
{φ : RoughForm I M F k}
{s : Set M}
{x : M}
(hs : UniqueMDiffAt[s] x)
(hφ : DifferentiableWithinAt ℝ (φ.inChartAt x) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x))
:
mextDerivWithin (RoughForm.mapCoeff L φ) s x = L.compContinuousAlternatingMap (mextDerivWithin φ s x)
The exterior derivative is natural in the coefficient space, at a point where the coordinate expression of the form is differentiable within the set.
theorem
TauCeti.mextDeriv_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
[IsManifold I 1 M]
(L : F →L[ℝ] G)
{φ : RoughForm I M F k}
(hφ : IsSmoothForm I 1 φ)
:
The exterior derivative of a C¹ form is natural in the coefficient space.
@[simp]
theorem
TauCeti.mpullbackWithin_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
[TopologicalSpace M']
[ChartedSpace H' M']
{I' : ModelWithCorners ℝ E' H'}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(L : F →L[ℝ] G)
(f : M → M')
(s : Set M)
(η : RoughForm I' M' F k)
:
mpullbackWithin I I' f s (RoughForm.mapCoeff L η) = RoughForm.mapCoeff L (mpullbackWithin I I' f s η)
Coefficient maps commute with within-set pullback.
@[simp]
theorem
TauCeti.mpullback_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
[TopologicalSpace M']
[ChartedSpace H' M']
{I' : ModelWithCorners ℝ E' H'}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(L : F →L[ℝ] G)
(f : M → M')
(η : RoughForm I' M' F k)
:
Coefficient maps commute with pullback.
Coefficient maps of smooth forms #
noncomputable def
TauCeti.SmoothForm.mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
[IsManifold I 1 M]
(L : F →L[ℝ] G)
:
A continuous linear map of coefficient spaces, as a linear map on smooth forms.
Instances For
@[simp]
theorem
TauCeti.SmoothForm.coe_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
[IsManifold I 1 M]
(L : F →L[ℝ] G)
(φ : SmoothForm I M F k)
:
The underlying rough form of a coefficient map of a smooth form.
@[simp]
theorem
TauCeti.SmoothForm.mapCoeff_id
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
:
theorem
TauCeti.SmoothForm.mapCoeff_comp
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
{G' : Type u_9}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup G']
[NormedSpace ℝ G']
{k : ℕ}
[IsManifold I 1 M]
(L' : G →L[ℝ] G')
(L : F →L[ℝ] G)
:
theorem
TauCeti.SmoothForm.mapCoeff_cast
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
[IsManifold I 1 M]
{l : ℕ}
(h : k = l)
(L : F →L[ℝ] G)
(φ : SmoothForm I M F k)
:
Coefficient maps of smooth forms commute with transport of the degree.
@[simp]
theorem
TauCeti.SmoothForm.mextDerivₗ_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
[IsManifold I 1 M]
[IsManifold I 2 M]
(L : F →L[ℝ] G)
(φ : SmoothForm I M F k)
:
The exterior derivative of smooth forms is natural in the coefficient space.
@[simp]
theorem
TauCeti.SmoothForm.mpullback_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
[TopologicalSpace M']
[ChartedSpace H' M']
{I' : ModelWithCorners ℝ E' H'}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
[IsManifold I 1 M]
[IsManifold I' 1 M']
(L : F →L[ℝ] G)
(f : M → M')
(hf : ContMDiff I I' (↑⊤) f)
(φ : SmoothForm I' M' F k)
:
Coefficient maps commute with pullback of smooth forms.
Scalars acting on the coefficients #
@[instance_reducible]
noncomputable instance
TauCeti.SmoothForm.instSMul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
{S : Type u_10}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
:
SMul S (SmoothForm I M F k)
Scalars acting on the coefficients act on smooth forms pointwise.
@[simp]
theorem
TauCeti.SmoothForm.smul_toRoughForm
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
{S : Type u_10}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
(c : S)
(φ : SmoothForm I M F k)
:
The rough form underlying a scalar multiple of a smooth form is the scalar multiple of its rough form.
theorem
TauCeti.SmoothForm.eval₂_smul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[IsManifold I 1 M]
{S : Type u_10}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
(c : S)
(φ : SmoothForm I M F 2)
(x : M)
(v w : TangentSpace I x)
:
Evaluating a scalar multiple of a degree-two smooth form scales the evaluation.
theorem
TauCeti.SmoothForm.smul_eq_mapCoeff
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
{S : Type u_10}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
(c : S)
(φ : SmoothForm I M F k)
:
Scalar multiplication of a smooth form is the coefficient map given by multiplication by the scalar.
@[instance_reducible]
noncomputable instance
TauCeti.SmoothForm.instModule
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
{S : Type u_10}
[Semiring S]
[Module S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
:
Module S (SmoothForm I M F k)
Scalars acting on the coefficients act on smooth forms, making them a module. For complex coefficients this is the complex vector space of complex-valued smooth forms.
instance
TauCeti.SmoothForm.instIsScalarTowerReal
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
{S : Type u_10}
[SMul ℝ S]
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
[IsScalarTower ℝ S F]
:
IsScalarTower ℝ S (SmoothForm I M F k)
When the coefficient scalars restrict to real scalars, so do their actions on smooth forms;
for complex coefficients, RCLike.real_smul_eq_coe_smul then identifies the real action on
smooth forms with the action of real numbers viewed as complex numbers.
instance
TauCeti.SmoothForm.instSMulCommClassReal
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
{S : Type u_10}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
:
SMulCommClass ℝ S (SmoothForm I M F k)
instance
TauCeti.SmoothForm.instSMulCommClassReal_1
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
{S : Type u_10}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
:
SMulCommClass S ℝ (SmoothForm I M F k)
theorem
TauCeti.SmoothForm.mapCoeff_smul_of_map_smul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
{G : Type u_8}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
[IsManifold I 1 M]
{S : Type u_10}
{S' : Type u_11}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
[Monoid S']
[DistribMulAction S' G]
[ContinuousConstSMul S' G]
[SMulCommClass ℝ S' G]
(L : F →L[ℝ] G)
{c : S}
{d : S'}
(hL : ∀ (v : F), L (c • v) = d • L v)
(φ : SmoothForm I M F k)
:
A coefficient map that is semilinear for scalars c ↦ d turns multiplication of smooth
forms by c into multiplication by d.
@[simp]
theorem
TauCeti.SmoothForm.mextDerivₗ_smul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
{S : Type u_10}
[IsManifold I 2 M]
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
(c : S)
(φ : SmoothForm I M F k)
:
The exterior derivative of smooth forms is linear for scalars acting on the coefficients, such as complex scalars on complex-valued forms.
@[simp]
theorem
TauCeti.SmoothForm.mpullback_smul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
{E' : Type u_4}
{H' : Type u_5}
{M' : Type u_6}
{F : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[TopologicalSpace H']
[TopologicalSpace M']
[ChartedSpace H' M']
{I' : ModelWithCorners ℝ E' H'}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{k : ℕ}
[IsManifold I 1 M]
[IsManifold I' 1 M']
{S : Type u_10}
[Monoid S]
[DistribMulAction S F]
[ContinuousConstSMul S F]
[SMulCommClass ℝ S F]
(f : M → M')
(hf : ContMDiff I I' (↑⊤) f)
(c : S)
(φ : SmoothForm I' M' F k)
:
Pullback of smooth forms is linear for scalars acting on the coefficients.
theorem
TauCeti.SmoothForm.mapCoeff_conj_smul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
{k : ℕ}
[IsManifold I 1 M]
(c : ℂ)
(φ : SmoothForm I M ℂ k)
:
Complex conjugation of the coefficients of complex-valued smooth forms is conjugate-linear.
Coefficient maps and scalars of wedge products #
theorem
TauCeti.RoughForm.mapCoeff_wedgeWith
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
{k : ℕ}
{F₁ : Type u_10}
{F₂ : Type u_11}
{F₃ : Type u_12}
{G₁ : Type u_13}
{G₂ : Type u_14}
{G₃ : Type u_15}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
[NormedAddCommGroup G₁]
[NormedSpace ℝ G₁]
[NormedAddCommGroup G₂]
[NormedSpace ℝ G₂]
[NormedAddCommGroup G₃]
[NormedSpace ℝ G₃]
{l : ℕ}
(μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃)
(μ' : G₁ →L[ℝ] G₂ →L[ℝ] G₃)
(L₁ : F₁ →L[ℝ] G₁)
(L₂ : F₂ →L[ℝ] G₂)
(L : F₃ →L[ℝ] G₃)
(hL : ∀ (a : F₁) (b : F₂), L ((μ a) b) = (μ' (L₁ a)) (L₂ b))
(φ : RoughForm I M F₁ k)
(ψ : RoughForm I M F₂ l)
:
The paired rough-form wedge is natural in the coefficients: if coefficient maps L₁, L₂,
L intertwine the pairings μ and μ', then the coefficient map L of the wedge of φ and ψ
is the wedge of their coefficient maps.
theorem
TauCeti.SmoothForm.mapCoeff_wedgeWith
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
{k : ℕ}
{F₁ : Type u_10}
{F₂ : Type u_11}
{F₃ : Type u_12}
{G₁ : Type u_13}
{G₂ : Type u_14}
{G₃ : Type u_15}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
[NormedAddCommGroup G₁]
[NormedSpace ℝ G₁]
[NormedAddCommGroup G₂]
[NormedSpace ℝ G₂]
[NormedAddCommGroup G₃]
[NormedSpace ℝ G₃]
{l : ℕ}
[IsManifold I 1 M]
(μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃)
(μ' : G₁ →L[ℝ] G₂ →L[ℝ] G₃)
(L₁ : F₁ →L[ℝ] G₁)
(L₂ : F₂ →L[ℝ] G₂)
(L : F₃ →L[ℝ] G₃)
(hL : ∀ (a : F₁) (b : F₂), L ((μ a) b) = (μ' (L₁ a)) (L₂ b))
(φ : SmoothForm I M F₁ k)
(ψ : SmoothForm I M F₂ l)
:
The paired wedge of smooth forms is natural in the coefficients: if coefficient maps L₁,
L₂, L intertwine the pairings μ and μ', then the coefficient map L of the wedge of φ
and ψ is the wedge of their coefficient maps.
theorem
TauCeti.SmoothForm.wedgeWith_smul_left_of_map_smul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
{k : ℕ}
{F₁ : Type u_10}
{F₂ : Type u_11}
{F₃ : Type u_12}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{l : ℕ}
[IsManifold I 1 M]
{S : Type u_16}
{S' : Type u_17}
[Monoid S']
[DistribMulAction S' F₃]
[ContinuousConstSMul S' F₃]
[SMulCommClass ℝ S' F₃]
[Monoid S]
[DistribMulAction S F₁]
[ContinuousConstSMul S F₁]
[SMulCommClass ℝ S F₁]
(μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃)
{c : S}
{d : S'}
(hcd : ∀ (a : F₁) (b : F₂), (μ (c • a)) b = d • (μ a) b)
(φ : SmoothForm I M F₁ k)
(ψ : SmoothForm I M F₂ l)
:
If the pairing turns multiplication by c in its first argument into multiplication by d,
then so does the paired wedge of smooth forms in its first form. For a complex-bilinear pairing
of complex coefficient spaces this is complex-linearity in the first form; it also covers
pairings that are conjugate-linear in the first argument.
theorem
TauCeti.SmoothForm.wedgeWith_smul_right_of_map_smul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
{k : ℕ}
{F₁ : Type u_10}
{F₂ : Type u_11}
{F₃ : Type u_12}
[NormedAddCommGroup F₁]
[NormedSpace ℝ F₁]
[NormedAddCommGroup F₂]
[NormedSpace ℝ F₂]
[NormedAddCommGroup F₃]
[NormedSpace ℝ F₃]
{l : ℕ}
[IsManifold I 1 M]
{S : Type u_16}
{S' : Type u_17}
[Monoid S']
[DistribMulAction S' F₃]
[ContinuousConstSMul S' F₃]
[SMulCommClass ℝ S' F₃]
[Monoid S]
[DistribMulAction S F₂]
[ContinuousConstSMul S F₂]
[SMulCommClass ℝ S F₂]
(μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃)
{c : S}
{d : S'}
(hcd : ∀ (a : F₁) (b : F₂), (μ a) (c • b) = d • (μ a) b)
(φ : SmoothForm I M F₁ k)
(ψ : SmoothForm I M F₂ l)
:
If the pairing turns multiplication by c in its second argument into multiplication by
d, then so does the paired wedge of smooth forms in its second form. For a complex-bilinear
pairing of complex coefficient spaces this is complex-linearity in the second form.
theorem
TauCeti.SmoothForm.mapCoeff_conj_wedgeWith_mul
{E : Type u_1}
{H : Type u_2}
{M : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
{k l : ℕ}
[IsManifold I 1 M]
(φ : SmoothForm I M ℂ k)
(ψ : SmoothForm I M ℂ l)
:
(mapCoeff ↑Complex.conjCLE) (((wedgeWith (ContinuousLinearMap.mul ℝ ℂ)) φ) ψ) = ((wedgeWith (ContinuousLinearMap.mul ℝ ℂ)) ((mapCoeff ↑Complex.conjCLE) φ)) ((mapCoeff ↑Complex.conjCLE) ψ)
Complex conjugation of the coefficients of complex-valued smooth forms is multiplicative for the wedge product given by complex multiplication.