Documentation

TauCeti.LinearAlgebra.TotallyReal.Finrank

The dimension of a totally real subspace #

A totally real subspace L for a linear endomorphism J is disjoint from its J-image, and a maximal totally real subspace is complementary to it (TauCeti.LinearAlgebra.TotallyReal.Basic). When J is injective on L, L and J(L) have the same dimension, so these two conditions become dimension statements: a totally real subspace has at most half the dimension of the ambient space, and a maximal totally real subspace has exactly half (TauCeti.IsTotallyReal.isMaximalTotallyReal_iff_two_mul_finrank_eq).

This is the linear-algebra half of the statement that the totally real tori T_α, T_β in the symmetric product Sym^g(Σ) of a Heegaard surface are g-dimensional in the 2g-dimensional Sym^g(Σ) (Ozsváth--Szabó, arXiv:math/0101206, Section 2); the corresponding half-dimensionality of Lagrangian subspaces is the same count. Nothing here needs a symplectic form or an almost complex structure: only injectivity of J on L is used, which is automatic when J² = -1.

Main declarations #

source
theorem TauCeti.IsTotallyReal.two_mul_finrank_le {R : Type u_1} {E : Type u_2} [DivisionRing R] [AddCommGroup E] [Module R E] [FiniteDimensional R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsTotallyReal J L) (hJ : Function.Injective ⇑(J.domRestrict L)) :
2 * Module.finrank R ↥L ≤ Module.finrank R E

A totally real subspace has at most half the dimension of the ambient space.

source
theorem TauCeti.IsTotallyReal.isMaximalTotallyReal {R : Type u_1} {E : Type u_2} [DivisionRing R] [AddCommGroup E] [Module R E] [FiniteDimensional R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsTotallyReal J L) (hJ : Function.Injective ⇑(J.domRestrict L)) (hdim : 2 * Module.finrank R ↥L = Module.finrank R E) :
IsMaximalTotallyReal J L

A totally real subspace of exactly half the ambient dimension is maximal totally real: the dimension count forces the sum L ⊔ J(L) to be everything.

source
theorem TauCeti.IsMaximalTotallyReal.two_mul_finrank_eq {R : Type u_1} {E : Type u_2} [DivisionRing R] [AddCommGroup E] [Module R E] [FiniteDimensional R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) (hJ : Function.Injective ⇑(J.domRestrict L)) :
2 * Module.finrank R ↥L = Module.finrank R E

A maximal totally real subspace has exactly half the dimension of the ambient space.

source
theorem TauCeti.IsMaximalTotallyReal.even_finrank {R : Type u_1} {E : Type u_2} [DivisionRing R] [AddCommGroup E] [Module R E] [FiniteDimensional R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) (hJ : Function.Injective ⇑(J.domRestrict L)) :
Even (Module.finrank R E)

The ambient space of a maximal totally real subspace is even-dimensional.

source
theorem TauCeti.IsMaximalTotallyReal.finrank_eq_half {R : Type u_1} {E : Type u_2} [DivisionRing R] [AddCommGroup E] [Module R E] [FiniteDimensional R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) (hJ : Function.Injective ⇑(J.domRestrict L)) :
Module.finrank R ↥L = Module.finrank R E / 2

A maximal totally real subspace is half-dimensional.

source
theorem TauCeti.IsTotallyReal.isMaximalTotallyReal_iff_two_mul_finrank_eq {R : Type u_1} {E : Type u_2} [DivisionRing R] [AddCommGroup E] [Module R E] [FiniteDimensional R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsTotallyReal J L) (hJ : Function.Injective ⇑(J.domRestrict L)) :
IsMaximalTotallyReal J L ↔ 2 * Module.finrank R ↥L = Module.finrank R E

A totally real subspace is maximal totally real exactly when it is half-dimensional.