Theorems · Definition · linear algebra

Submodule.Quotient.equiv

{R : Type u_1} →
  [inst : Ring R] →
    {R₂ : Type u_5} →
      [inst_1 : Ring R₂] →
        {σ₁₂ : R →+* R₂} →
          {σ₂₁ : R₂ →+* R} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M : Type u_6} →
                  {N : Type u_7} →
                    [inst_4 : AddCommGroup M] →
                      [inst_5 : Module R M] →
                        [inst_6 : AddCommGroup N] →
                          [inst_7 : Module R₂ N] →
                            (P : Submodule R M) →
                              (Q : Submodule R₂ N) →
                                (f : M ≃ₛₗ[σ₁₂] N) → Submodule.map (↑f) P = Q → (M ⧸ P) ≃ₛₗ[σ₁₂] N ⧸ Q

If P is a submodule of M and Q a submodule of N, and f : M ≃ₛₗ[σ] N maps P to Q, then M ⧸ P is equivalent to N ⧸ Q.

Defined in

Mathlib.LinearAlgebra.Quotient.Basic

Cited by

9 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRingRingHomInvPairRingHomInvPairAddCommGroupModuleAddCommGroupModule