Documentation

TauCeti.Geometry.Symplectic.Rescale

Rescaling symplectic forms #

A nonzero scalar multiple of a symplectic form is again symplectic. This file records that pointwise linear-algebra operation and the basic interaction with the tame and compatible almost-complex predicates.

Positive rescalings preserve the positivity condition 0 < ω(v, J v) and hence preserve tameness and compatibility. Negative rescalings do not preserve tameness for the same J, but they do preserve invariance because invariance is linear in the form.

Main declarations #

The convention is the standard one from symplectic geometry: changing the overall positive scale of ω changes the metric scale but not the compatible almost complex structure.

source
noncomputable def TauCeti.SymplecticForm.rescale {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (c : ℝ) (hc : c ≠ 0) :
SymplecticForm V

The nonzero scalar multiple c • ω of a symplectic form.

The hypothesis c ≠ 0 is needed for nondegeneracy. The construction is not an instance because there is no closed scalar action at c = 0.

Instances For
    source
    @[simp]
    theorem TauCeti.SymplecticForm.rescale_toBilinForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).toBilinForm = c • ω.toBilinForm
    source
    @[simp]
    theorem TauCeti.SymplecticForm.rescale_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (c : ℝ) (hc : c ≠ 0) (v w : V) :
    (fun (v w : V) => ((ω.rescale c hc).toBilinForm v) w) v w = c * (fun (v w : V) => (ω.toBilinForm v) w) v w

    Evaluation of a rescaled symplectic form.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.rescale_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (h : 1 ≠ 0) :
    ω.rescale 1 h = ω
    source
    @[simp]
    theorem TauCeti.SymplecticForm.rescale_rescale {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (c d : ℝ) (hc : c ≠ 0) (hd : d ≠ 0) :
    (ω.rescale c hc).rescale d hd = ω.rescale (d * c) ⋯

    Successive nonzero rescalings multiply the scale factors.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.orthogonal_rescale {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).orthogonal L = ω.orthogonal L

    Nonzero rescaling leaves the symplectic complement of a subspace unchanged.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.isIsotropic_rescale_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).IsIsotropic L ↔ ω.IsIsotropic L

    Nonzero rescaling preserves and reflects isotropic subspaces.

    source
    theorem TauCeti.SymplecticForm.IsIsotropic.rescale {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsIsotropic L) (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).IsIsotropic L

    Isotropy is preserved by nonzero rescaling of the symplectic form.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.isCoisotropic_rescale_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).IsCoisotropic L ↔ ω.IsCoisotropic L

    Nonzero rescaling preserves and reflects coisotropic subspaces.

    source
    theorem TauCeti.SymplecticForm.IsCoisotropic.rescale {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsCoisotropic L) (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).IsCoisotropic L

    Coisotropy is preserved by nonzero rescaling of the symplectic form.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.isLagrangian_rescale_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).IsLagrangian L ↔ ω.IsLagrangian L

    Nonzero rescaling preserves and reflects Lagrangian subspaces.

    source
    theorem TauCeti.SymplecticForm.IsLagrangian.rescale {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsLagrangian L) (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).IsLagrangian L

    Lagrangian subspaces are preserved by nonzero rescaling of the symplectic form.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.isSymplectic_rescale_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).IsSymplectic L ↔ ω.IsSymplectic L

    Nonzero rescaling preserves and reflects symplectic subspaces.

    source
    theorem TauCeti.SymplecticForm.IsSymplectic.rescale {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {L : Submodule ℝ V} (h : ω.IsSymplectic L) (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).IsSymplectic L

    Symplectic subspaces are preserved by nonzero rescaling of the symplectic form.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.rescale_associatedBilinForm_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (c : ℝ) (hc : c ≠ 0) (v w : V) :
    (((ω.rescale c hc).associatedBilinForm J) v) w = c * ((ω.associatedBilinForm J) v) w

    The associated bilinear form of a rescaled symplectic form is rescaled by the same factor.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.invariant_rescale_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).Invariant J ↔ ω.Invariant J

    Rescaling by a nonzero scalar preserves and reflects J-invariance.

    source
    theorem TauCeti.SymplecticForm.Invariant.rescale {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Invariant J) (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).Invariant J

    J-invariance is preserved by any nonzero rescaling of the symplectic form.

    source
    theorem TauCeti.SymplecticForm.invariant_rescale_neg_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (c : ℝ) (hc : c ≠ 0) :
    (ω.rescale c hc).Invariant (-J) ↔ ω.Invariant J

    Rescaling by a nonzero scalar and replacing J by -J preserves and reflects J-invariance.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.tames_rescale_iff_of_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} {c : ℝ} (hcpos : 0 < c) :
    (ω.rescale c ⋯).Tames J ↔ ω.Tames J

    Positive rescaling preserves and reflects tameness.

    source
    theorem TauCeti.SymplecticForm.Tames.rescale_of_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Tames J) {c : ℝ} (hcpos : 0 < c) :
    (ω.rescale c ⋯).Tames J

    Tameness is preserved by positive rescaling of the symplectic form.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.tames_rescale_neg_iff_of_neg {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} {c : ℝ} (hcneg : c < 0) :
    (ω.rescale c ⋯).Tames (-J) ↔ ω.Tames J

    Negative rescaling preserves and reflects tameness after replacing J by -J.

    source
    theorem TauCeti.SymplecticForm.Tames.rescale_neg_of_neg {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Tames J) {c : ℝ} (hcneg : c < 0) :
    (ω.rescale c ⋯).Tames (-J)

    Tameness is preserved by negative rescaling if the almost complex structure is negated too.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.compatible_rescale_iff_of_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} {c : ℝ} (hcpos : 0 < c) :
    (ω.rescale c ⋯).Compatible J ↔ ω.Compatible J

    Positive rescaling preserves and reflects compatibility.

    source
    theorem TauCeti.SymplecticForm.Compatible.rescale_of_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) {c : ℝ} (hcpos : 0 < c) :
    (ω.rescale c ⋯).Compatible J

    Compatibility is preserved by positive rescaling of the symplectic form.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.compatible_rescale_neg_iff_of_neg {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} {c : ℝ} (hcneg : c < 0) :
    (ω.rescale c ⋯).Compatible (-J) ↔ ω.Compatible J

    Negative rescaling preserves and reflects compatibility after replacing J by -J.

    source
    theorem TauCeti.SymplecticForm.Compatible.rescale_neg_of_neg {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) {c : ℝ} (hcneg : c < 0) :
    (ω.rescale c ⋯).Compatible (-J)

    Compatibility is preserved by negative rescaling if the almost complex structure is negated too.