Base-change models of rational subspaces and their quotients

Pure and mixed Hodge structures live on an integral module Vℤ together with abstract models Vℚ and Vℂ of its rational and complex scalar extensions. To regard a sub-object or a quotient of such a structure — a kernel, an image, a cokernel — as a structure of the same kind, one needs the same three carriers for it. This file builds them for a rational subspace U ⊆ Vℚ:

• the sub-object is carried by the integral vectors integralSubmodule ιℚ U of U, by U itself, and by the complexification rationalToComplexSubmodule hℚ hℂ U of U;
• the quotient is carried by Vℤ ⧸ integralSubmodule ιℚ U, by Vℚ ⧸ U, and by Vℂ ⧸ rationalToComplexSubmodule hℚ hℂ U.

In both cases the restricted, respectively induced, structure maps are base changes. For the rational model of the sub-object this is the statement that U is the localization of its integral vectors, since a rational vector becomes integral after clearing a denominator; it holds without any freeness or torsion hypothesis on Vℤ. The complex model of the sub-object follows from the tower ℤ → ℚ → ℂ, and both quotient models from right exactness of the tensor product. The inputs are Mathlib's localization of submodules (Submodule.localized' and its Galois insertion Submodule.localized'gi), isLocalizedModule_iff_isBaseChange, and IsBaseChange.of_right_exact.

The models are compatible with the ambient data: the complexification of the inclusion U → Vℚ and of the projection Vℚ → Vℚ ⧸ U are the inclusion and the projection of the complex models, and the lattice conjugation of each model is the one induced by the ambient lattice conjugation.

Main declarations

• TauCeti.Hodge.integralSubmodule: the integral vectors of a rational subspace.
• TauCeti.Hodge.isBaseChange_integralSubmoduleToRational and TauCeti.Hodge.isBaseChange_integralSubmoduleToComplex: a rational subspace and its complexification are the rational and complex scalar extensions of its integral vectors.
• TauCeti.Hodge.isBaseChange_integralQuotientToRational and TauCeti.Hodge.isBaseChange_integralQuotientToComplex: the same for the quotients.
• TauCeti.Hodge.rationalMapToComplex_subtype and TauCeti.Hodge.rationalMapToComplex_mkQ: the inclusion and the projection complexify to the inclusion and the projection.
• TauCeti.Hodge.rationalToComplexSubmodule_comap_subtype: complexification commutes with taking the trace of a rational subspace on another.
• TauCeti.Hodge.rationalToComplexSubmodule_map_mkQ: complexification commutes with passing to the image of a rational subspace in a quotient.
• TauCeti.Hodge.latticeConjugation_integralSubmoduleToComplex and TauCeti.Hodge.latticeConjugation_integralQuotientToComplex: the lattice conjugations of the models are induced by the ambient one.

def TauCeti.Hodge.integralSubmodule {Vℤ : Type u} {Vℚ : Type v} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] (ιℚ : Vℤ →ₗ[ℤ] Vℚ) (U : Submodule ℚ Vℚ) : Submodule ℤ Vℤ

The integral vectors of a rational subspace U: those vectors of the integral module whose rationalization lies in U.

@[simp]

theorem TauCeti.Hodge.mem_integralSubmodule {Vℤ : Type u} {Vℚ : Type v} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {U : Submodule ℚ Vℚ} {x : Vℤ} : x ∈ integralSubmodule ιℚ U ↔ ιℚ x ∈ U

def TauCeti.Hodge.integralSubmoduleToRational {Vℤ : Type u} {Vℚ : Type v} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] (ιℚ : Vℤ →ₗ[ℤ] Vℚ) (U : Submodule ℚ Vℚ) : ↥(integralSubmodule ιℚ U) →ₗ[ℤ] ↥U

The rationalization map restricted to the integral vectors of a rational subspace.

@[simp]

theorem TauCeti.Hodge.coe_integralSubmoduleToRational {Vℤ : Type u} {Vℚ : Type v} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} (U : Submodule ℚ Vℚ) (x : ↥(integralSubmodule ιℚ U)) : ↑((integralSubmoduleToRational ιℚ U) x) = ιℚ ↑x

def TauCeti.Hodge.integralQuotientToRational {Vℤ : Type u} {Vℚ : Type v} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] (ιℚ : Vℤ →ₗ[ℤ] Vℚ) (U : Submodule ℚ Vℚ) : Vℤ ⧸ integralSubmodule ιℚ U →ₗ[ℤ] Vℚ ⧸ U

The map induced by rationalization on the quotients by a rational subspace and by its integral vectors.

@[simp]

theorem TauCeti.Hodge.integralQuotientToRational_mk {Vℤ : Type u} {Vℚ : Type v} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} (U : Submodule ℚ Vℚ) (x : Vℤ) : (integralQuotientToRational ιℚ U) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (ιℚ x)

theorem TauCeti.Hodge.isBaseChange_integralSubmoduleToRational {Vℤ : Type u} {Vℚ : Type v} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} (hℚ : IsBaseChange ℚ ιℚ) (U : Submodule ℚ Vℚ) : IsBaseChange ℚ (integralSubmoduleToRational ιℚ U)

A rational subspace is the localization, hence the rational scalar extension, of its integral vectors.

theorem TauCeti.Hodge.isBaseChange_integralQuotientToRational {Vℤ : Type u} {Vℚ : Type v} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} (hℚ : IsBaseChange ℚ ιℚ) (U : Submodule ℚ Vℚ) : IsBaseChange ℚ (integralQuotientToRational ιℚ U)

The quotient of the rational model by a rational subspace is the rational scalar extension of the quotient of the integral module by the integral vectors of that subspace.

theorem TauCeti.Hodge.ι_mem_rationalToComplexSubmodule {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) {U : Submodule ℚ Vℚ} {x : Vℤ} (hx : x ∈ integralSubmodule ιℚ U) : ιℂ x ∈ rationalToComplexSubmodule hℚ hℂ U

The complexification map carries the integral vectors of a rational subspace into its complexification.

noncomputable def TauCeti.Hodge.integralSubmoduleToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) : ↥(integralSubmodule ιℚ U) →ₗ[ℤ] ↥(rationalToComplexSubmodule hℚ hℂ U)

The complexification map restricted to the integral vectors of a rational subspace, with values in the complexification of that subspace.

@[simp]

theorem TauCeti.Hodge.coe_integralSubmoduleToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) (x : ↥(integralSubmodule ιℚ U)) : ↑((integralSubmoduleToComplex hℚ hℂ U) x) = ιℂ ↑x

noncomputable def TauCeti.Hodge.integralQuotientToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) : Vℤ ⧸ integralSubmodule ιℚ U →ₗ[ℤ] Vℂ ⧸ rationalToComplexSubmodule hℚ hℂ U

The map induced by complexification on the quotients by the complexification of a rational subspace and by its integral vectors.

@[simp]

theorem TauCeti.Hodge.integralQuotientToComplex_mk {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) (x : Vℤ) : (integralQuotientToComplex hℚ hℂ U) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (ιℂ x)

theorem TauCeti.Hodge.isBaseChange_integralSubmoduleToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) : IsBaseChange ℂ (integralSubmoduleToComplex hℚ hℂ U)

The complexification of a rational subspace is the complex scalar extension of its integral vectors: extend first to U over ℚ, then to the complexification of U over ℂ.

theorem TauCeti.Hodge.isBaseChange_integralQuotientToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) : IsBaseChange ℂ (integralQuotientToComplex hℚ hℂ U)

The quotient of the complex model by the complexification of a rational subspace is the complex scalar extension of the quotient of the integral module by the integral vectors of that subspace.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_subtype {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) : rationalMapToComplex ⋯ ⋯ hℚ hℂ U.subtype = (rationalToComplexSubmodule hℚ hℂ U).subtype

Complexifying the inclusion of a rational subspace, between the models of the subspace and the ambient models, gives the inclusion of its complexification.

@[simp]

theorem TauCeti.Hodge.rationalMapToComplex_mkQ {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) : rationalMapToComplex hℚ hℂ ⋯ ⋯ U.mkQ = (rationalToComplexSubmodule hℚ hℂ U).mkQ

Complexifying the projection onto the quotient by a rational subspace, between the ambient models and the models of the quotient, gives the projection onto the quotient by its complexification.

theorem TauCeti.Hodge.rationalToComplexSubmodule_comap_subtype {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U V : Submodule ℚ Vℚ) : rationalToComplexSubmodule ⋯ ⋯ (Submodule.comap U.subtype V) = Submodule.comap (rationalToComplexSubmodule hℚ hℂ U).subtype (rationalToComplexSubmodule hℚ hℂ V)

Complexifying the trace of a rational subspace V on a rational subspace U gives the trace of the complexification of V on the complexification of U.

@[simp]

theorem TauCeti.Hodge.rationalToComplexSubmodule_map_mkQ {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U V : Submodule ℚ Vℚ) : rationalToComplexSubmodule ⋯ ⋯ (Submodule.map U.mkQ V) = Submodule.map (rationalToComplexSubmodule hℚ hℂ U).mkQ (rationalToComplexSubmodule hℚ hℂ V)

Complexifying the image of a rational subspace in a quotient gives the image of its complexification in the corresponding complex quotient.

theorem TauCeti.Hodge.latticeConjugation_mem_rationalToComplexSubmodule {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) (x : Vℂ) : x ∈ rationalToComplexSubmodule hℚ hℂ U → (latticeConjugation hℂ).toEquiv x ∈ rationalToComplexSubmodule hℚ hℂ U

Lattice conjugation preserves the complexification of a rational subspace, in the form taken by TauCeti.Hodge.Conjugation.restrict and TauCeti.Hodge.Conjugation.quotient.

@[simp]

theorem TauCeti.Hodge.coe_latticeConj_integralSubmoduleToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) (x : ↥(rationalToComplexSubmodule hℚ hℂ U)) : ↑((latticeConj ⋯) x) = (latticeConj hℂ) ↑x

Lattice conjugation on the complex model of a rational subspace is computed in the ambient complex model.

@[simp]

theorem TauCeti.Hodge.latticeConj_integralQuotientToComplex_mk {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) (x : Vℂ) : (latticeConj ⋯) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((latticeConj hℂ) x)

Lattice conjugation on the complex model of a quotient by a rational subspace acts on classes through the ambient lattice conjugation.

@[simp]

theorem TauCeti.Hodge.map_latticeConj_integralQuotientToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) (A : Submodule ℂ Vℂ) : Submodule.map (latticeConj ⋯) (Submodule.map (rationalToComplexSubmodule hℚ hℂ U).mkQ A) = Submodule.map (rationalToComplexSubmodule hℚ hℂ U).mkQ (Submodule.map (latticeConj hℂ) A)

Conjugating the image of a complex subspace in a quotient is the image of its conjugate.

theorem TauCeti.Hodge.latticeConjugation_integralSubmoduleToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) : latticeConjugation ⋯ = (latticeConjugation hℂ).restrict ⋯

The lattice conjugation of the complex model of a rational subspace is the restriction of the ambient lattice conjugation.

theorem TauCeti.Hodge.latticeConjugation_integralQuotientToComplex {Vℤ : Type u} {Vℚ : Type v} {Vℂ : Type w} [AddCommGroup Vℤ] [AddCommGroup Vℚ] [Module ℚ Vℚ] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℚ : Vℤ →ₗ[ℤ] Vℚ} {ιℂ : Vℤ →ₗ[ℤ] Vℂ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (U : Submodule ℚ Vℚ) : latticeConjugation ⋯ = (latticeConjugation hℂ).quotient ⋯

The lattice conjugation of the complex model of a quotient by a rational subspace is induced by the ambient lattice conjugation.