The group structure on the translation orbit space of a submodule

A submodule p of a module M over a ring acts on M by translation, and the orbit space of this action is the standard carrier AddAction.orbitRel.Quotient p M for quotients of M by translations, for instance for a complex torus E ⧸ Λ built from a lattice Λ in a complex vector space E. Two points lie in one orbit exactly when their difference lies in p, which is also the relation defining the quotient module M ⧸ p.

This file transfers the additive group structure of M ⧸ p to the orbit space, so that the orbit projection is additive, and records the resulting additive equivalence between the two quotients. A semilinear map carrying p into a submodule q then induces an additive map of orbit spaces, read through these equivalences from Submodule.mapQ, and a semilinear equivalence carrying p onto q induces an additive equivalence. For lattices L ⊆ E and L' ⊆ E' in complex vector spaces, these are the group homomorphisms and isomorphisms of complex tori E / L → E' / L' underlying the holomorphic maps induced by complex linear maps preserving the lattices.

For a linear map f : M → M₂ and a submodule q of M₂, the image f⁻¹(q) / p of f⁻¹(q) in the orbit space contains the image of ker f, and the quotient of the former by the latter is (q ∩ range f) / (q ∩ f(p)), which is (q ∩ range f) / f(p) when f(p) ⊆ q. For lattices L ⊆ E, L' ⊆ E' in complex vector spaces and a complex linear map f with f(L) ⊆ L', this is the component group of f⁻¹(L') / L, the kernel of the induced homomorphism of complex tori E / L → E' / L': when f(p) ⊆ q, the subgroup f⁻¹(q) / p is exactly the kernel of the map of orbit spaces induced by f.

The orbit space of translation by a product p.prod q on M × M₂ is additively equivalent to the product of the orbit spaces of p and q, compatibly with the maps induced by products of linear maps.

Main declarations

• Submodule.orbitRelQuotientAddEquiv: the orbit space of translation by p is additively equivalent to the quotient module M ⧸ p, by an equivalence sending the orbit of x to the class of x.
• Submodule.orbitRelQuotient_mk_add, Submodule.orbitRelQuotient_mk_zero, Submodule.orbitRelQuotient_mk_neg, Submodule.orbitRelQuotient_mk_sub: the orbit projection is additive.
• Submodule.orbitRelQuotient_mk_eq_mk_iff: two points have the same orbit exactly when their difference lies in p.
• Submodule.orbitRelQuotient_mk_eq_zero_iff: its kernel is p.
• Submodule.orbitRelQuotientMkHom: the orbit projection as an additive map.
• LinearMap.exact_orbitRelQuotientMkHom_range: for a linear map f, the sequence N → M → M / range f is exact.
• Submodule.orbitRelQuotientMap: the additive map of orbit spaces induced by a semilinear map f carrying p into q, functorial in f (Submodule.orbitRelQuotientMap_id, Submodule.orbitRelQuotientMap_comp).
• Submodule.orbitRelQuotientMap_injective_iff: the induced map is injective exactly when f⁻¹(q) ≤ p.
• Submodule.ker_orbitRelQuotientMap: the kernel of the induced map is the image f⁻¹(q) / p of f⁻¹(q).
• Submodule.orbitRelQuotientCongr: the additive equivalence of orbit spaces induced by a semilinear equivalence e with p.map e = q.
• Submodule.orbitRelQuotientMap_bijective_iff: for a semilinear equivalence e carrying p into q, the induced map is bijective exactly when e carries p onto q.
• Submodule.orbitRelQuotientComapQuotientEquiv: the quotient of f⁻¹(q) / p by the image of ker f is additively equivalent to (q ∩ range f) / (q ∩ f(p)).
• Submodule.orbitRelQuotientProdAddEquiv: the orbit space of translation by p.prod q is additively equivalent to the product of the orbit spaces of p and q.
• Submodule.orbitRelQuotientProdAddEquiv_orbitRelQuotientMap_prodMap: through this equivalence, the map induced by f.prodMap g is the product of the maps induced by f and g.

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.orbitRel_apply_iff_sub_mem {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {x y : M} : (AddAction.orbitRel (↥p) M) x y ↔ x - y ∈ p

Two points lie in one orbit of translation by a submodule p exactly when their difference lies in p.

@[instance_reducible]

instance Submodule.instAddCommGroupOrbitRelQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : AddCommGroup (AddAction.orbitRel.Quotient (↥p) M)

The additive group structure on the orbit space of translation by p, transferred from the quotient module M ⧸ p, which is the same quotient of M.

def Submodule.orbitRelQuotientAddEquiv {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : AddAction.orbitRel.Quotient (↥p) M ≃+ M ⧸ p

The orbit space of translation by p is additively equivalent to the quotient module M ⧸ p, by an equivalence sending the orbit of x to the class of x.

@[simp]

theorem Submodule.orbitRelQuotientAddEquiv_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (x : M) : p.orbitRelQuotientAddEquiv ⟦x⟧ = Quotient.mk x

Submodule.orbitRelQuotientAddEquiv sends the orbit of x to the class of x.

@[simp]

theorem Submodule.orbitRelQuotientAddEquiv_symm_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (x : M) : p.orbitRelQuotientAddEquiv.symm (Quotient.mk x) = ⟦x⟧

The inverse of Submodule.orbitRelQuotientAddEquiv sends the class of x to the orbit of x.

@[simp]

theorem Submodule.orbitRelQuotient_mk_add {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (x y : M) : ⟦x + y⟧ = ⟦x⟧ + ⟦y⟧

The orbit projection for translation by p is additive.

@[simp]

theorem Submodule.orbitRelQuotient_mk_zero {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : ⟦0⟧ = 0

The orbit projection for translation by p sends 0 to 0.

def Submodule.orbitRelQuotientMkHom {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : M →+ AddAction.orbitRel.Quotient (↥p) M

The orbit projection M → AddAction.orbitRel.Quotient p M for translation by p, as an additive map.

@[simp]

theorem Submodule.coe_orbitRelQuotientMkHom {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : ⇑p.orbitRelQuotientMkHom = _root_.Quotient.mk (AddAction.orbitRel (↥p) M)

As a function, Submodule.orbitRelQuotientMkHom is the orbit projection.

theorem Submodule.orbitRelQuotient_mk_eq_mk_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {x y : M} : ⟦x⟧ = ⟦y⟧ ↔ x - y ∈ p

Two points of M have the same image in the orbit space of translation by p exactly when their difference lies in p.

@[simp]

theorem Submodule.orbitRelQuotient_mk_eq_zero_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {x : M} : ⟦x⟧ = 0 ↔ x ∈ p

A point of M projects to 0 in the orbit space of translation by p exactly when it lies in p.

@[simp]

theorem Submodule.ker_orbitRelQuotientMkHom {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : p.orbitRelQuotientMkHom.ker = p.toAddSubgroup

The kernel of the orbit projection for translation by p is p.

theorem LinearMap.exact_orbitRelQuotientMkHom_range {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : N →ₗ[R] M) : Function.Exact ⇑f ⇑f.range.orbitRelQuotientMkHom

The period sequence is exact: for a linear map f : N → M, the orbit projection for translation by the range of f is exact after f, in N → M → M / range f. Read through Submodule.orbitRelQuotientAddEquiv, this is LinearMap.exact_map_mkQ_range.

@[simp]

theorem Submodule.orbitRelQuotient_mk_neg {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (x : M) : ⟦-x⟧ = -⟦x⟧

The orbit projection for translation by p commutes with negation.

@[simp]

theorem Submodule.orbitRelQuotient_mk_sub {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (x y : M) : ⟦x - y⟧ = ⟦x⟧ - ⟦y⟧

The orbit projection for translation by p commutes with subtraction.

def Submodule.orbitRelQuotientMap {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ comap f q) : AddAction.orbitRel.Quotient (↥p) M →+ AddAction.orbitRel.Quotient (↥q) M₂

A semilinear map f : M → M₂ carrying p into q induces an additive map from the orbit space of translation by p to that of translation by q, sending the orbit of x to the orbit of f x. It is Submodule.mapQ read through Submodule.orbitRelQuotientAddEquiv.

@[simp]

theorem Submodule.orbitRelQuotientMap_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ comap f q) (x : M) : (p.orbitRelQuotientMap q f h) ⟦x⟧ = ⟦f x⟧

Submodule.orbitRelQuotientMap sends the orbit of x to the orbit of f x.

@[simp]

theorem Submodule.orbitRelQuotientAddEquiv_orbitRelQuotientMap {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ comap f q) (x : AddAction.orbitRel.Quotient (↥p) M) : q.orbitRelQuotientAddEquiv ((p.orbitRelQuotientMap q f h) x) = (p.mapQ q f h) (p.orbitRelQuotientAddEquiv x)

Read through Submodule.orbitRelQuotientAddEquiv, the induced map of orbit spaces is Submodule.mapQ.

@[simp]

theorem Submodule.orbitRelQuotientMap_id {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (h : p ≤ comap LinearMap.id p := ⋯) : p.orbitRelQuotientMap p LinearMap.id h = AddMonoidHom.id (AddAction.orbitRel.Quotient (↥p) M)

The identity map induces the identity of the orbit space.

theorem Submodule.orbitRelQuotientMap_comp {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {τ₁₂ : R →+* R₂} {R₃ : Type u_5} {M₃ : Type u_6} [Ring R₃] [AddCommGroup M₃] [Module R₃ M₃] (r : Submodule R₃ M₃) {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : p ≤ comap f q) (hg : q ≤ comap g r) (h : p ≤ comap f (comap g r) := ⋯) : p.orbitRelQuotientMap r (g ∘ₛₗ f) h = (q.orbitRelQuotientMap r g hg).comp (p.orbitRelQuotientMap q f hf)

The map of orbit spaces induced by a composite is the composite of the induced maps.

theorem Submodule.orbitRelQuotientMap_injective_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ comap f q) : Function.Injective ⇑(p.orbitRelQuotientMap q f h) ↔ comap f q ≤ p

The map of orbit spaces induced by f is injective exactly when every point that f sends into q already lies in p.

theorem Submodule.orbitRelQuotientMap_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : Function.Surjective ⇑f) (h : p ≤ comap f q) : Function.Surjective ⇑(p.orbitRelQuotientMap q f h)

The map of orbit spaces induced by a surjective map is surjective.

theorem Submodule.ker_orbitRelQuotientMap {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ comap f q) : (p.orbitRelQuotientMap q f h).ker = AddSubgroup.map p.orbitRelQuotientMkHom (comap f q).toAddSubgroup

The kernel of the map of orbit spaces induced by f is the image f⁻¹(q) / p of f⁻¹(q) in the orbit space of translation by p. For lattices and a complex linear map, it is the kernel of the induced homomorphism of complex tori.

theorem Submodule.range_orbitRelQuotientMap {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ comap f q) : Set.range ⇑(p.orbitRelQuotientMap q f h) = _root_.Quotient.mk (AddAction.orbitRel (↥q) M₂) '' Set.range ⇑f

The range of the map of orbit spaces induced by f is the image of the range of f.

def Submodule.orbitRelQuotientCongr {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M ≃ₛₗ[σ₁₂] M₂) (he : map (↑e) p = q) : AddAction.orbitRel.Quotient (↥p) M ≃+ AddAction.orbitRel.Quotient (↥q) M₂

A semilinear equivalence e : M ≃ M₂ carrying p onto q induces an additive equivalence between the orbit spaces of translation by p and by q, sending the orbit of x to the orbit of e x. It is Submodule.Quotient.equiv read through Submodule.orbitRelQuotientAddEquiv.

@[simp]

theorem Submodule.orbitRelQuotientCongr_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M ≃ₛₗ[σ₁₂] M₂) (he : map (↑e) p = q) (x : M) : (p.orbitRelQuotientCongr q e he) ⟦x⟧ = ⟦e x⟧

Submodule.orbitRelQuotientCongr sends the orbit of x to the orbit of e x.

@[simp]

theorem Submodule.orbitRelQuotientCongr_symm {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M ≃ₛₗ[σ₁₂] M₂) (he : map (↑e) p = q) : (p.orbitRelQuotientCongr q e he).symm = q.orbitRelQuotientCongr p e.symm ⋯

The inverse of the equivalence induced by e is the equivalence induced by e.symm.

@[simp]

theorem Submodule.coe_orbitRelQuotientCongr {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M ≃ₛₗ[σ₁₂] M₂) (he : map (↑e) p = q) : ↑(p.orbitRelQuotientCongr q e he) = p.orbitRelQuotientMap q ↑e ⋯

As an additive map, the equivalence induced by e is the map of orbit spaces induced by e.

theorem Submodule.orbitRelQuotientMap_bijective_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] (q : Submodule R₂ M₂) {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M ≃ₛₗ[σ₁₂] M₂) (h : p ≤ comap (↑e) q) : Function.Bijective ⇑(p.orbitRelQuotientMap q (↑e) h) ↔ map (↑e) p = q

For a semilinear equivalence e carrying p into q, the induced map of orbit spaces is bijective exactly when e carries p onto q.

noncomputable def Submodule.orbitRelQuotientComapQuotientEquiv {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] (q : Submodule R M₂) (f : M →ₗ[R] M₂) : ↥(AddSubgroup.map p.orbitRelQuotientMkHom (comap f q).toAddSubgroup) ⧸ (AddSubgroup.map p.orbitRelQuotientMkHom f.ker.toAddSubgroup).addSubgroupOf (AddSubgroup.map p.orbitRelQuotientMkHom (comap f q).toAddSubgroup) ≃+ ↥(q ⊓ f.range) ⧸ comap (q ⊓ f.range).subtype (map f p)

For a linear map f : M → M₂ and submodules p ≤ M, q ≤ M₂, consider the image K of f⁻¹(q) and the image K₀ of ker f in the orbit space of translation by p. The quotient K / K₀ is additively equivalent to (q ∩ range f) / (q ∩ f(p)), by the map sending the class of the orbit of x ∈ f⁻¹(q) to the class of f x. Here the denominator q ∩ f(p) is the pullback of f(p) to q ∩ range f; it is f(p) itself when f(p) ⊆ q.

For lattices L ⊆ E, L' ⊆ E' and a complex linear map f with f(L) ⊆ L', K = f⁻¹(L') / L is the kernel of the induced homomorphism of complex tori E / L → E' / L', K₀ is its identity component, and this is the description of its component group as (L' ∩ range f) / f(L).

@[simp]

theorem Submodule.orbitRelQuotientComapQuotientEquiv_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] (q : Submodule R M₂) (f : M →ₗ[R] M₂) {x : M} (hx : x ∈ comap f q) : (p.orbitRelQuotientComapQuotientEquiv q f) ↑⟨⟦x⟧, ⋯⟩ = Quotient.mk ⟨f x, ⋯⟩

Submodule.orbitRelQuotientComapQuotientEquiv sends the class of the orbit of x ∈ f⁻¹(q) to the class of f x.

theorem Submodule.orbitRel_prod {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] (q : Submodule R M₂) : AddAction.orbitRel (↥(p.prod q)) (M × M₂) = (AddAction.orbitRel (↥p) M).prod (AddAction.orbitRel (↥q) M₂)

The orbit relation of translation by p.prod q on M × M₂ is the product of the orbit relations of translation by p on M and by q on M₂.

def Submodule.orbitRelQuotientProdAddEquiv {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] (q : Submodule R M₂) : AddAction.orbitRel.Quotient (↥(p.prod q)) (M × M₂) ≃+ AddAction.orbitRel.Quotient (↥p) M × AddAction.orbitRel.Quotient (↥q) M₂

The orbit space of translation by p.prod q on M × M₂ is additively equivalent to the product of the orbit spaces of translation by p on M and by q on M₂, by the equivalence sending the orbit of (x, y) to the pair of orbits of x and y. For lattices L ⊆ E and L' ⊆ E' in complex vector spaces, this identifies the complex torus (E × E') / (L × L') with the product of the complex tori E / L and E' / L'.

@[simp]

theorem Submodule.orbitRelQuotientProdAddEquiv_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] (q : Submodule R M₂) (x : M × M₂) : (p.orbitRelQuotientProdAddEquiv q) ⟦x⟧ = (⟦x.1⟧, ⟦x.2⟧)

Submodule.orbitRelQuotientProdAddEquiv sends the orbit of x to the pair of orbits of its components.

@[simp]

theorem Submodule.orbitRelQuotientProdAddEquiv_symm_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] (q : Submodule R M₂) (x : M) (y : M₂) : (p.orbitRelQuotientProdAddEquiv q).symm (⟦x⟧, ⟦y⟧) = ⟦(x, y)⟧

The inverse of Submodule.orbitRelQuotientProdAddEquiv sends a pair of orbits of x and y to the orbit of (x, y).

@[simp]

theorem Submodule.orbitRelQuotientProdAddEquiv_orbitRelQuotientMap_prodMap {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] (q : Submodule R M₂) {N : Type u_4} {N₂ : Type u_5} [AddCommGroup N] [Module R N] [AddCommGroup N₂] [Module R N₂] (r : Submodule R N) (r₂ : Submodule R N₂) (f : M →ₗ[R] N) (g : M₂ →ₗ[R] N₂) (hf : p ≤ comap f r) (hg : q ≤ comap g r₂) (h : p.prod q ≤ comap (f.prodMap g) (r.prod r₂) := ⋯) (x : AddAction.orbitRel.Quotient (↥(p.prod q)) (M × M₂)) : (r.orbitRelQuotientProdAddEquiv r₂) (((p.prod q).orbitRelQuotientMap (r.prod r₂) (f.prodMap g) h) x) = Prod.map (⇑(p.orbitRelQuotientMap r f hf)) (⇑(q.orbitRelQuotientMap r₂ g hg)) ((p.orbitRelQuotientProdAddEquiv q) x)

The map of orbit spaces induced by a product f.prodMap g is, through Submodule.orbitRelQuotientProdAddEquiv, the product of the maps induced by f and by g. For lattices and complex linear maps, the homomorphism of complex tori induced by f × g is the product of the homomorphisms induced by f and g.