Documentation

TauCeti.Geometry.Hodge.Realification

Realification of an integral module #

The realification of an integral module V is the scalar extension ℝ ⊗[ℤ] V. If an abstract complexification Vℂ of the same module is given through IsBaseChange, associativity of scalar extension identifies ℂ ⊗[ℝ] (ℝ ⊗[ℤ] V) with Vℂ. This equivalence intertwines ordinary conjugation on the left with the lattice-induced conjugation on the right.

The comparison is the base-change bridge needed to transfer real linear data on an integral module, such as an almost complex structure or the real scalar extension of an integral bilinear form, to its chosen abstract complexification. Under it the real points of the lattice-induced conjugation are exactly the image of the realification, 1 ⊗ₜ x, and a complexified integral form takes on them the values of its real scalar extension.

Main declarations #

source
@[reducible, inline]
abbrev TauCeti.Hodge.Realification (V : Type u) [AddCommGroup V] :
Type u

The realification ℝ ⊗[ℤ] V of an integral module.

Instances For
    source
    def TauCeti.Hodge.realificationMap {V : Type u} [AddCommGroup V] :
    V →ₗ[ℤ] Realification V

    The canonical map from an integral module to its realification.

    Instances For
      source
      @[simp]
      theorem TauCeti.Hodge.realificationMap_apply {V : Type u} [AddCommGroup V] (x : V) :
      realificationMap x = 1 ⊗ₜ[ℤ] x

      The canonical map to the realification sends an integral vector to the corresponding pure tensor.

      source
      theorem TauCeti.Hodge.realificationMap_injective {V : Type u} [AddCommGroup V] [Module.Flat ℤ V] :
      Function.Injective ⇑realificationMap

      The canonical map to the realification is injective when the integral module is flat, in particular when it is free.

      source
      noncomputable def TauCeti.Hodge.realificationComplexEquiv {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) :
      TensorProduct ℝ ℂ (Realification V) ≃ₗ[ℂ] Vℂ

      The canonical comparison from the complexification of the realification to an abstract complexification of the original integral module.

      Instances For
        source
        @[simp]
        theorem TauCeti.Hodge.realificationComplexEquiv_tmul_tmul {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (z : ℂ) (r : ℝ) (x : V) :
        (realificationComplexEquiv hℂ) (z ⊗ₜ[ℝ] (r ⊗ₜ[ℤ] x)) = (z * ↑r) • ιℂ x

        The realification comparison sends a nested pure tensor to scalar multiplication of the corresponding integral vector.

        source
        theorem TauCeti.Hodge.realificationComplexEquiv_one_tmul_realificationMap {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (x : V) :
        (realificationComplexEquiv hℂ) (1 ⊗ₜ[ℝ] realificationMap x) = ιℂ x

        Passing an integral vector through realification and then complexification gives its image in the chosen abstract complexification.

        source
        @[simp]
        theorem TauCeti.Hodge.realificationComplexEquiv_symm_ι {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (x : V) :
        (realificationComplexEquiv hℂ).symm (ιℂ x) = 1 ⊗ₜ[ℝ] (1 ⊗ₜ[ℤ] x)

        The inverse comparison sends an integral vector of the abstract complexification to the corresponding nested pure tensor.

        source
        @[simp]
        theorem TauCeti.Hodge.realificationComplexEquiv_conj {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (x : TensorProduct ℝ ℂ (Realification V)) :
        (realificationComplexEquiv hℂ) ((tmulConj (Realification V)) x) = (latticeConj hℂ) ((realificationComplexEquiv hℂ) x)

        The comparison between the iterated and abstract complexifications intertwines their conjugations.

        source
        @[simp]
        theorem TauCeti.Hodge.realificationComplexEquiv_symm_conj {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (x : Vℂ) :
        (realificationComplexEquiv hℂ).symm ((latticeConj hℂ) x) = (tmulConj (Realification V)) ((realificationComplexEquiv hℂ).symm x)

        The inverse realification comparison intertwines lattice-induced conjugation with ordinary conjugation.

        The real points of the abstract complexification #

        source
        @[simp]
        theorem TauCeti.Hodge.latticeConj_realificationComplexEquiv_one_tmul {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (x : Realification V) :
        (latticeConj hℂ) ((realificationComplexEquiv hℂ) (1 ⊗ₜ[ℝ] x)) = (realificationComplexEquiv hℂ) (1 ⊗ₜ[ℝ] x)

        Lattice-induced conjugation fixes the image of a real vector under the realification comparison.

        source
        theorem TauCeti.Hodge.exists_eq_realificationComplexEquiv_one_tmul {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) {y : Vℂ} (hy : y ∈ realPoints (latticeConj hℂ)) :
        ∃ (x : Realification V), y = (realificationComplexEquiv hℂ) (1 ⊗ₜ[ℝ] x)

        The real points of the abstract complexification are the realification. Every vector fixed by the lattice-induced conjugation is the image of a real vector under the realification comparison.

        source
        @[simp]
        theorem TauCeti.Hodge.bilinForm_realificationComplexEquiv_one_tmul {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (Q : LinearMap.BilinForm ℤ V) (x y : Realification V) :
        ((hℂ.bilinForm Q) ((realificationComplexEquiv hℂ) (1 ⊗ₜ[ℝ] x))) ((realificationComplexEquiv hℂ) (1 ⊗ₜ[ℝ] y)) = ↑(((LinearMap.BilinForm.baseChange ℝ Q) x) y)

        On real points a complexified integral form is the real scalar extension of the form. The complexification of an integral bilinear form, evaluated on the images of two real vectors under the realification comparison, is the real scalar extension of the form evaluated on those vectors.