Totally real linear subspaces

This file supplies the linear-algebra notion of a (maximal) totally real subspace with respect to a linear endomorphism J over an arbitrary scalar semiring. This is the algebraic pointwise model for totally real boundary conditions in the analytic Heegaard Floer roadmap: a boundary tangent space L is totally real when it is disjoint from its J-image, and maximal totally real when the two are moreover complementary. The terminology is borrowed from the usual real-linear situation, but the complement API itself is purely module-theoretic.

No integrability, topology, or symplectic form is bundled here.

def TauCeti.IsTotallyReal {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] (J : E →ₗ[R] E) (L : Submodule R E) : Prop

A submodule is totally real with respect to J if it is disjoint from its J-image.

Equations

• TauCeti.IsTotallyReal J L = Disjoint L (Submodule.map J L)

@[simp]

theorem TauCeti.isTotallyReal_iff {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] (J : E →ₗ[R] E) (L : Submodule R E) : IsTotallyReal J L ↔ Disjoint L (Submodule.map J L)

The totally real predicate unfolds to disjointness of L and its J-image.

def TauCeti.IsMaximalTotallyReal {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] (J : E →ₗ[R] E) (L : Submodule R E) : Prop

A submodule is maximal totally real with respect to J if it is complementary to its J-image.

Equations

• TauCeti.IsMaximalTotallyReal J L = IsCompl L (Submodule.map J L)

@[simp]

theorem TauCeti.isMaximalTotallyReal_iff {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] (J : E →ₗ[R] E) (L : Submodule R E) : IsMaximalTotallyReal J L ↔ IsCompl L (Submodule.map J L)

The maximal totally real predicate unfolds to complementarity of L and its J-image.

theorem TauCeti.IsTotallyReal.disjoint {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsTotallyReal J L) : Disjoint L (Submodule.map J L)

A totally real submodule is disjoint from its J-image.

theorem TauCeti.IsTotallyReal.inf_eq_bot {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsTotallyReal J L) : L ⊓ Submodule.map J L = ⊥

The intersection of a totally real submodule with its J-image is bottom.

theorem TauCeti.IsTotallyReal.bot {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] (J : E →ₗ[R] E) : IsTotallyReal J ⊥

The zero submodule is totally real for any J.

theorem TauCeti.IsTotallyReal.mono {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsTotallyReal J L) {L' : Submodule R E} (h : L' ≤ L) : IsTotallyReal J L'

A submodule of a totally real submodule is totally real.

theorem TauCeti.IsTotallyReal.prod {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] {J : E →ₗ[R] E} {L : Submodule R E} {K : F →ₗ[R] F} {M : Submodule R F} (hL : IsTotallyReal J L) (hM : IsTotallyReal K M) : IsTotallyReal (J.prodMap K) (L.prod M)

Products of totally real submodules are totally real for LinearMap.prodMap.

theorem TauCeti.IsTotallyReal.map {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] {J : E →ₗ[R] E} {L : Submodule R E} {K : F →ₗ[R] F} (hL : IsTotallyReal J L) {f : E →ₗ[R] F} (hf : Function.Injective ⇑f) (hfJ : f ∘ₗ J = K ∘ₗ f) : IsTotallyReal K (Submodule.map f L)

An injective linear map intertwining J and K sends J-totally real submodules to K-totally real submodules. For real-linear maps between complex vector spaces, with J and K multiplication by i, the intertwining condition says that the map is complex-linear.

theorem TauCeti.IsMaximalTotallyReal.isCompl {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) : IsCompl L (Submodule.map J L)

A maximal totally real submodule is complementary to its J-image.

theorem TauCeti.IsMaximalTotallyReal.disjoint {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) : Disjoint L (Submodule.map J L)

A maximal totally real submodule is disjoint from its J-image.

theorem TauCeti.IsMaximalTotallyReal.isTotallyReal {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) : IsTotallyReal J L

A maximal totally real submodule is in particular totally real.

theorem TauCeti.IsMaximalTotallyReal.inf_eq_bot {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) : L ⊓ Submodule.map J L = ⊥

The intersection of a maximal totally real submodule with its J-image is bottom.

theorem TauCeti.IsMaximalTotallyReal.codisjoint {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) : Codisjoint L (Submodule.map J L)

A maximal totally real submodule spans codisjointly with its J-image.

theorem TauCeti.IsMaximalTotallyReal.sup_eq_top {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) : L ⊔ Submodule.map J L = ⊤

A maximal totally real submodule and its J-image span the whole module.

theorem TauCeti.IsMaximalTotallyReal.prod {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] {J : E →ₗ[R] E} {K : F →ₗ[R] F} {L : Submodule R E} {M : Submodule R F} (hL : IsMaximalTotallyReal J L) (hM : IsMaximalTotallyReal K M) : IsMaximalTotallyReal (J.prodMap K) (L.prod M)

Products of maximal totally real submodules are maximal totally real for LinearMap.prodMap.

@[simp]

theorem TauCeti.Submodule.map_prod_top_bot_skewSwap {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommGroup E] [Module R E] : Submodule.map (↑(LinearEquiv.skewSwap R E E)) (⊤.prod ⊥) = ⊥.prod ⊤

The image of the first coordinate factor under the standard doubled-module complex structure is the second coordinate factor.

@[simp]

theorem TauCeti.Submodule.map_prod_bot_top_skewSwap {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommGroup E] [Module R E] : Submodule.map (↑(LinearEquiv.skewSwap R E E)) (⊥.prod ⊤) = ⊤.prod ⊥

The image of the second coordinate factor under the standard doubled-module complex structure is the first coordinate factor.

theorem TauCeti.Submodule.isMaximalTotallyReal_prod_top_bot_skewSwap {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommGroup E] [Module R E] : IsMaximalTotallyReal (↑(LinearEquiv.skewSwap R E E)) (⊤.prod ⊥)

The first factor in E × E is maximal totally real for the standard doubled-module complex structure.

theorem TauCeti.Submodule.isMaximalTotallyReal_prod_bot_top_skewSwap {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommGroup E] [Module R E] : IsMaximalTotallyReal (↑(LinearEquiv.skewSwap R E E)) (⊥.prod ⊤)

The second factor in E × E is maximal totally real for the standard doubled-module complex structure.

theorem TauCeti.IsTotallyReal.image {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsTotallyReal J L) (hJ : J ∘ₗ J = -LinearMap.id) : IsTotallyReal J (Submodule.map J L)

If J² = -1, the image J(L) is totally real whenever L is totally real.

theorem TauCeti.IsTotallyReal.image_iff {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hJ : J ∘ₗ J = -LinearMap.id) : IsTotallyReal J (Submodule.map J L) ↔ IsTotallyReal J L

Under J² = -1, L is totally real if and only if its image J(L) is totally real.

theorem TauCeti.IsMaximalTotallyReal.image {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) (hJ : J ∘ₗ J = -LinearMap.id) : IsMaximalTotallyReal J (Submodule.map J L)

If J² = -1, the image J(L) is maximal totally real whenever L is maximal totally real.

theorem TauCeti.IsMaximalTotallyReal.image_iff {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hJ : J ∘ₗ J = -LinearMap.id) : IsMaximalTotallyReal J (Submodule.map J L) ↔ IsMaximalTotallyReal J L

Under J² = -1, L is maximal totally real if and only if its image J(L) is maximal totally real.

theorem TauCeti.IsMaximalTotallyReal.existsUnique_add {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {J : E →ₗ[R] E} {L : Submodule R E} (hL : IsMaximalTotallyReal J L) (x : E) : ∃! y : ↥L × ↥(Submodule.map J L), ↑y.1 + ↑y.2 = x

Every vector decomposes uniquely as an element of L plus an element of J(L).