The preimage of a discrete subgroup modulo a subgroup

Let E be a real topological vector space, L a subgroup of E, and f : E → E' a continuous linear map, over a ring K such as ℝ or ℂ, which carries L into a discrete subgroup L' of E'. In the orbit space E / L of translation by L, consider the subgroup f⁻¹(L') / L. This file shows that it is closed when L' is closed, and that its identity component is the image of ker f. Combined with Submodule.orbitRelQuotientComapQuotientEquiv, which identifies the quotient of f⁻¹(L') / L by the image of ker f with (L' ∩ range f) / f(L), this describes the component group of f⁻¹(L') / L.

For lattices L ⊆ E and L' ⊆ E' in complex vector spaces and a complex linear map f with f(L) ⊆ L', the subgroup f⁻¹(L') / L is the kernel of the homomorphism of complex tori E / L → E' / L' induced by f. Its identity component is the image of ker f, which as a group is ker f / (L ∩ ker f), a complex torus because L ∩ ker f is a full lattice in ker f (ZLattice.isZLattice_comap_ker_subtype); its component group is (L' ∩ range f) / f(L).

Main results

• Submodule.isClosed_orbitRelQuotient_mk_image_preimage: f⁻¹(L') / L is closed in E / L.
• Submodule.exists_isOpen_inter_orbitRelQuotient_mk_image_preimage: the image of ker f is relatively open in f⁻¹(L') / L.
• Submodule.connectedComponentIn_orbitRelQuotient_mk_image_preimage: the connected component of 0 in f⁻¹(L') / L is the image of ker f.
• Submodule.coe_addSubgroupOf_eq_connectedComponent_zero: the same statement inside the subgroup f⁻¹(L') / L, in the form used by Submodule.orbitRelQuotientComapQuotientEquiv.
• Submodule.range_orbitRelQuotientMap_ker_subtype: for normed spaces and continuous f, the image of ker f / (L ∩ ker f) → E / L is the identity component of the kernel of the map E / L → E' / L' induced by f.

References

• Christina Birkenhake and Herbert Lange, Complex Abelian Varieties, second edition, Grundlehren der mathematischen Wissenschaften 302, Springer, 2004, Chapter 1, Section 1.2.

theorem Submodule.isClosed_orbitRelQuotient_mk_image_preimage {K : Type u_1} [Ring K] {E : Type u_2} [AddCommGroup E] [Module K E] {E' : Type u_3} [AddCommGroup E'] [Module K E'] (L : Submodule ℤ E) {L' : Submodule ℤ E'} (f : E →ₗ[K] E') [TopologicalSpace E] [TopologicalSpace E'] (hL' : IsClosed ↑L') (hfc : Continuous ⇑f) (hf : map (↑ℤ f) L ≤ L') : IsClosed (_root_.Quotient.mk (AddAction.orbitRel (↥L) E) '' ⇑f ⁻¹' ↑L')

If f carries L into the closed subgroup L', then f⁻¹(L') / L is closed in the orbit space of translation by L. For lattices and a complex linear f, it is the kernel of the induced homomorphism of complex tori.

theorem Submodule.exists_isOpen_inter_orbitRelQuotient_mk_image_preimage {K : Type u_1} [Ring K] {E : Type u_2} [AddCommGroup E] [Module K E] {E' : Type u_3} [AddCommGroup E'] [Module K E'] (L : Submodule ℤ E) {L' : Submodule ℤ E'} (f : E →ₗ[K] E') [TopologicalSpace E] [TopologicalSpace E'] [ContinuousAdd E] [ContinuousAdd E'] [DiscreteTopology ↥L'] (hfc : Continuous ⇑f) (hf : map (↑ℤ f) L ≤ L') : ∃ (U : Set (AddAction.orbitRel.Quotient (↥L) E)), IsOpen U ∧ U ∩ _root_.Quotient.mk (AddAction.orbitRel (↥L) E) '' ⇑f ⁻¹' ↑L' = _root_.Quotient.mk (AddAction.orbitRel (↥L) E) '' ↑f.ker

If f carries L into the discrete subgroup L', then the image of ker f is relatively open in f⁻¹(L') / L: it is the trace on f⁻¹(L') / L of an open subset of the orbit space of translation by L. For lattices and a complex linear f, the image of ker f is the identity component of the kernel of the induced homomorphism of complex tori, which is therefore an open subgroup of that kernel.

theorem Submodule.connectedComponentIn_orbitRelQuotient_mk_image_preimage {K : Type u_1} [Ring K] {E : Type u_2} [AddCommGroup E] [Module K E] {E' : Type u_3} [AddCommGroup E'] [Module K E'] (L : Submodule ℤ E) {L' : Submodule ℤ E'} (f : E →ₗ[K] E') [TopologicalSpace E] [TopologicalSpace E'] [ContinuousAdd E] [Module ℝ K] [Module ℝ E] [ContinuousSMul ℝ E] [IsScalarTower ℝ K E] [ContinuousAdd E'] [DiscreteTopology ↥L'] (hfc : Continuous ⇑f) (hf : map (↑ℤ f) L ≤ L') : connectedComponentIn (_root_.Quotient.mk (AddAction.orbitRel (↥L) E) '' ⇑f ⁻¹' ↑L') 0 = _root_.Quotient.mk (AddAction.orbitRel (↥L) E) '' ↑f.ker

If f carries L into the discrete subgroup L', then the connected component of 0 in f⁻¹(L') / L, inside the orbit space of translation by L, is the image of ker f. For lattices and a complex linear f, this is the identity component of the kernel of the induced homomorphism of complex tori.

theorem Submodule.coe_addSubgroupOf_eq_connectedComponent_zero {K : Type u_1} [Ring K] {E : Type u_2} [AddCommGroup E] [Module K E] {E' : Type u_3} [AddCommGroup E'] [Module K E'] (L : Submodule ℤ E) {L' : Submodule ℤ E'} (f : E →ₗ[K] E') [TopologicalSpace E] [TopologicalSpace E'] [ContinuousAdd E] [Module ℝ K] [Module ℝ E] [ContinuousSMul ℝ E] [IsScalarTower ℝ K E] [ContinuousAdd E'] [DiscreteTopology ↥L'] (hfc : Continuous ⇑f) (hf : map (↑ℤ f) L ≤ L') : ↑((AddSubgroup.map L.orbitRelQuotientMkHom (↑ℤ f).ker.toAddSubgroup).addSubgroupOf (AddSubgroup.map L.orbitRelQuotientMkHom (comap (↑ℤ f) L').toAddSubgroup)) = connectedComponent 0

Inside the subgroup K = f⁻¹(L') / L of the orbit space of translation by L, the image of ker f is the connected component of 0. Thus the quotient of K by this image, which Submodule.orbitRelQuotientComapQuotientEquiv identifies with (L' ∩ range f) / f(L), is the component group of K.

theorem Submodule.range_orbitRelQuotientMap_ker_subtype {K : Type u_4} [NormedField K] [NormedSpace ℝ K] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace K E] [IsScalarTower ℝ K E] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace K E'] (L : Submodule ℤ E) {L' : Submodule ℤ E'} [DiscreteTopology ↥L'] (f : E →ₗ[K] E') (hfc : Continuous ⇑f) (h : L ≤ comap (↑ℤ f) L') : Set.range ⇑((ZLattice.comap K L f.ker.subtype).orbitRelQuotientMap L (↑ℤ f.ker.subtype) ⋯) = connectedComponentIn (↑(L.orbitRelQuotientMap L' (↑ℤ f) h).ker) 0

Let the continuous map f carry L into the discrete subgroup L'. The image of the map of quotients ker f / (L ∩ ker f) → E / L induced by the inclusion of ker f is the identity component of the kernel f⁻¹(L') / L of the map E / L → E' / L' induced by f. When L is a full lattice this map is a closed embedding (Submodule.isClosedEmbedding_orbitRelQuotientMap_subtype together with ZLattice.isZLattice_comap_ker_subtype), so this identity component is the torus ker f / (L ∩ ker f).