Maps induced on presented quotients in ModuleCat

An object A of ModuleCat R is frequently presented as a quotient X ⧸ p, by an isomorphism e : A ≅ ModuleCat.of R (X ⧸ p) together with a projection π : ModuleCat.of R X ⟶ A playing the role of Submodule.mkQ, in the sense that π ≫ e.hom = ModuleCat.ofHom p.mkQ. A linear map f : X₁ →ₗ[R] X₂ carrying p₁ into p₂ then induces a map A₁ ⟶ A₂, namely Submodule.mapQ conjugated by the two presentations.

This file records the one fact such an induced map is used through: it sends the class π₁ x of a representative to the class π₂ (f x), which is Mathlib's Submodule.mapQ_mkQ transported along the two presentations. Since the presentations are only given up to isomorphism, this characterisation — rather than a definitional unfolding — is how the induced map is computed.

Main statements

• ModuleCat.comp_conj_mapQ: the map induced by f on two presented quotients composed with the projection of the source is the projection of the target composed with f.

theorem ModuleCat.comp_conj_mapQ {R : Type v} [Ring R] {X₁ X₂ : Type u} [AddCommGroup X₁] [Module R X₁] [AddCommGroup X₂] [Module R X₂] {p₁ : Submodule R X₁} {p₂ : Submodule R X₂} {A₁ A₂ : ModuleCat R} (e₁ : A₁ ≅ ↧(X₁ ⧸ p₁)) (e₂ : A₂ ≅ ↧(X₂ ⧸ p₂)) {π₁ : ↧X₁ ⟶ A₁} {π₂ : ↧X₂ ⟶ A₂} (hπ₁ : CategoryTheory.CategoryStruct.comp π₁ e₁.hom = ofHom p₁.mkQ) (hπ₂ : CategoryTheory.CategoryStruct.comp π₂ e₂.hom = ofHom p₂.mkQ) (f : X₁ →ₗ[R] X₂) (hf : p₁ ≤ Submodule.comap f p₂) : CategoryTheory.CategoryStruct.comp π₁ (CategoryTheory.CategoryStruct.comp e₁.hom (CategoryTheory.CategoryStruct.comp (ofHom (p₁.mapQ p₂ f hf)) e₂.inv)) = CategoryTheory.CategoryStruct.comp (ofHom f) π₂

A map conjugated from Submodule.mapQ p₁ p₂ f along presentations e₁, e₂ of two objects as the quotients sends the class π₁ x of a representative to the class π₂ (f x). This is Submodule.mapQ_mkQ transported along the two presentations.