noncomputable def LieSubmodule.prodEquivOfIsCompl {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N N' : LieSubmodule R L M) (h : IsCompl N N') : ↥N × ↥N' ≃ₗ⁅R,L⁆ M

Equations

• N.prodEquivOfIsCompl N' h = { toLinearMap := ↑((↑N).prodEquivOfIsCompl ↑N' ⋯), map_lie' := ⋯, invFun := ((↑N).prodEquivOfIsCompl ↑N' ⋯).invFun, left_inv := ⋯, right_inv := ⋯ }

noncomputable def LieSubmodule.projectionOnto {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N N' : LieSubmodule R L M) (h : IsCompl N N') : M →ₗ⁅R,L⁆ ↥N

Equations

• N.projectionOnto N' h = (LieModuleHom.fst R L ↥N ↥N').comp (N.prodEquivOfIsCompl N' h).symm.toLieModuleHom

noncomputable def LieSubmodule.projection {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N N' : LieSubmodule R L M) (h : IsCompl N N') : M →ₗ⁅R,L⁆ M

Equations

• N.projection N' h = N.incl.comp (N.projectionOnto N' h)

@[simp]

theorem LieSubmodule.coe_projectionOnto_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N N' : LieSubmodule R L M} (h : IsCompl N N') (x : M) : ↑((N.projectionOnto N' h) x) = (N.projection N' h) x

theorem LieSubmodule.projection_add_projection_eq_self {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N N' : LieSubmodule R L M} (h : IsCompl N N') (x : M) : (N.projection N' h) x + (N'.projection N ⋯) x = x

theorem LieSubmodule.existsUnique_add_of_isCompl_prod {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N N' : LieSubmodule R L M} (h : IsCompl N N') (x : M) : ∃! u : ↥N × ↥N', ↑u.1 + ↑u.2 = x

@[simp]

theorem LieSubmodule.projection_apply_left {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N N' : LieSubmodule R L M} (h : IsCompl N N') (x : ↥N) : (N.projection N' h) ↑x = ↑x

@[simp]

theorem LieSubmodule.projection_apply_right {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N N' : LieSubmodule R L M} (h : IsCompl N N') (x : ↥N') : (N.projection N' h) ↑x = 0