mathlib3 documentation

linear_algebra.isomorphisms

Isomorphism theorems for modules. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The first and second isomorphism theorems for modules.

noncomputable def linear_map.quot_ker_equiv_range {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) :

The first isomorphism law for modules. The quotient of M by the kernel of f is linearly equivalent to the range of f.

Equations
noncomputable def linear_map.quot_ker_equiv_of_surjective {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) (hf : function.surjective f) :

The first isomorphism theorem for surjective linear maps.

Equations
@[simp]
theorem linear_map.quot_ker_equiv_range_apply_mk {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) (x : M) :
@[simp]
theorem linear_map.quot_ker_equiv_range_symm_apply_image {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂) (x : M) (h : f x linear_map.range f) :

Canonical linear map from the quotient p/(p ∩ p') to (p+p')/p', mapping x + (p ∩ p') to x + p', where p and p' are submodules of an ambient module.

Equations
noncomputable def linear_map.quotient_inf_equiv_sup_quotient {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p p' : submodule R M) :

Second Isomorphism Law : the canonical map from p/(p ∩ p') to (p+p')/p' as a linear isomorphism.

Equations

The third isomorphism theorem for modules.

def submodule.quotient_quotient_equiv_quotient_aux {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (S T : submodule R M) (h : S T) :

The map from the third isomorphism theorem for modules: (M / S) / (T / S) → M / T.

Equations
@[simp]
def submodule.quotient_quotient_equiv_quotient {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (S T : submodule R M) (h : S T) :
((M S) submodule.map S.mkq T) ≃ₗ[R] M T

Noether's third isomorphism theorem for modules: (M / S) / (T / S) ≃ M / T.

Equations
theorem submodule.card_quotient_mul_card_quotient {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (S T : submodule R M) (hST : T S) [decidable_pred (λ (x : M T), x submodule.map T.mkq S)] [fintype (M S)] [fintype (M T)] :

Corollary of the third isomorphism theorem: [S : T] [M : S] = [M : T]