theorem LieSubmodule.comap_comp {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] [LieRingModule L M] [LieRingModule L M₂] [LieRingModule L M₃] (f : M →ₗ⁅R,L⁆ M₂) (g : M₂ →ₗ⁅R,L⁆ M₃) (N : LieSubmodule R L M₃) : comap (g.comp f) N = comap f (comap g N)

theorem LieModuleHom.ker_comp {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] [LieRingModule L M] [LieRingModule L M₂] [LieRingModule L M₃] (f : M →ₗ⁅R,L⁆ M₂) (g : M₂ →ₗ⁅R,L⁆ M₃) : (g.comp f).ker = LieSubmodule.comap f g.ker

@[simp]

theorem LieSubmodule.mem_map_equiv {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) (N : LieSubmodule R L M) (x : M₂) : x ∈ map e.toLieModuleHom N ↔ e.symm x ∈ N

theorem LieSubmodule.map_equiv_eq_comap_symm {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) (N : LieSubmodule R L M) : map e.toLieModuleHom N = comap e.symm.toLieModuleHom N

theorem LieSubmodule.comap_equiv_eq_map_symm {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) (N : LieSubmodule R L M₂) : comap e.toLieModuleHom N = map e.symm.toLieModuleHom N

theorem LieModuleEquiv.toLieModuleHom_trans {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] [LieRingModule L M] [LieRingModule L M₂] [LieRingModule L M₃] (e : M ≃ₗ⁅R,L⁆ M₂) (e₂ : M₂ ≃ₗ⁅R,L⁆ M₃) : (e.trans e₂).toLieModuleHom = e₂.comp e.toLieModuleHom

@[simp]

theorem LieModuleEquiv.toLieModuleHom_refl {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : refl.toLieModuleHom = LieModuleHom.id

@[simp]

theorem LieModuleEquiv.comp_symm {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) : e.comp e.symm.toLieModuleHom = LieModuleHom.id

@[simp]

theorem LieModuleEquiv.symm_comp {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) : e.symm.comp e.toLieModuleHom = LieModuleHom.id