Invariant bilinear forms on a representation

A bilinear form B on the space of a representation ρ of G is invariant when every ρ g preserves it, B (ρ g x) (ρ g y) = B x y. The invariant forms are a submodule of all bilinear forms, and read as maps V → V* they are exactly the intertwiners from ρ to its dual representation -- the concrete form of the statement that they are the G-invariants of a space of bilinear forms. Cutting the invariant forms down by symmetry, respectively by alternation, gives two further submodules, and away from characteristic two they meet only in 0.

On an irreducible representation the invariant forms are tightly constrained, and the three constraints proved here are the ones the Frobenius-Schur trichotomy is read off from. First, the left radical of an invariant form is the kernel of an intertwiner out of an irreducible representation, so a nonzero invariant form on one is nondegenerate. Second, over an algebraically closed field and in finite dimensions, Schur's lemma makes a nonzero invariant form unique up to a scalar: the invariant forms are the line it spans. Third -- and this is the point -- the flip of an invariant form is invariant, so a nonzero invariant form is a scalar multiple of its own flip; flipping twice squares the scalar to 1, and the form is therefore either symmetric or the negative of its flip. Away from characteristic two the second alternative is exactly alternation, which gives the orthogonal/symplectic dichotomy: an irreducible representation carries at most a line of invariant forms, and -- in characteristic other than two -- any nonzero one on it is either symmetric or alternating.

Nothing here needs a finite group, and almost nothing needs finite dimensions: invariance, and the symmetric and alternating invariant forms with it, are defined for a representation of a monoid on a module over a commutative semiring, and only the results that invoke Schur's lemma ask for an algebraically closed field and a finite-dimensional space. The g⁻¹ in TauCeti.Representation.IsInvariantForm.apply_left, and with it the comparison with the dual representation, is what makes G a group.

Main definitions

• TauCeti.Representation.IsInvariantForm: B (ρ g x) (ρ g y) = B x y for all g, x, y.
• TauCeti.Representation.invariantForms: the invariant forms, as a submodule of BilinForm k V.
• TauCeti.Representation.symmetricInvariantForms and TauCeti.Representation.alternatingInvariantForms: the invariant forms that are symmetric, respectively alternating.
• TauCeti.Representation.invariantFormsEquivIntertwiningMapDual: the invariant forms of ρ as the intertwiners from ρ to its dual.

Main results

• TauCeti.Representation.isInvariantForm_iff_isIntertwiningMap: a form is invariant exactly when it intertwines ρ with ρ.dual.
• TauCeti.Representation.invariantForms_eq_invariants_linHom_dual: the invariant forms are the invariants of linHom ρ ρ.dual.
• TauCeti.Representation.symmetricInvariantForms_inf_alternatingInvariantForms: away from characteristic two the symmetric and the alternating invariant forms meet only in 0.
• TauCeti.Representation.IsInvariantForm.nondegenerate and TauCeti.Representation.IsInvariantForm.nondegenerate_iff_ne_zero: an invariant form on an irreducible representation is nondegenerate exactly when it is nonzero.
• TauCeti.Representation.IsInvariantForm.exists_eq_smul: over an algebraically closed field and in finite dimensions, an invariant form on an irreducible representation is a scalar multiple of any nonzero one.
• TauCeti.Representation.IsInvariantForm.invariantForms_eq_span: over an algebraically closed field and in finite dimensions, a nonzero invariant form on an irreducible representation spans all of them.
• TauCeti.Representation.IsInvariantForm.flip_eq_or_flip_eq_neg: in every characteristic, the flip of such a form is the form itself or its negative.
• TauCeti.Representation.IsInvariantForm.isSymm_or_isAlt: away from characteristic two -- the hypothesis (2 : k) ≠ 0 -- such a form is symmetric or alternating.
• TauCeti.Representation.exists_isSymm_or_exists_isAlt_or_invariantForms_eq_bot: the case split that dichotomy gives, that an irreducible representation carries a nonzero invariant symmetric form, or a nonzero invariant alternating one, or no nonzero invariant form at all.

Implementation notes

TauCeti.Representation.IsInvariantForm is the statement that every ρ g is an isometry of the form, TauCeti.BilinForm.IsIsometry B (ρ g), so that the invariant forms of a representation and the isometry group of a form are the same notion read two ways. Its body is not exposed: TauCeti.Representation.isInvariantForm_iff_isIsometry and TauCeti.Representation.isInvariantForm_iff introduce its isometry and pointwise forms, while TauCeti.Representation.IsInvariantForm.isIsometry and TauCeti.Representation.IsInvariantForm.apply eliminate them, so nothing outside this file has to unfold the definition. The pointwise iff is deliberately not a simp lemma: unfolding invariance into its quantified equation would take TauCeti.Representation.isInvariantForm_zero and TauCeti.Representation.mem_invariantForms out of simp-normal form, which the simpNF linter rejects. What the file adds around that pair is the two rewritings that are not immediate -- moving a single ρ g across the form at the cost of an inverse (TauCeti.Representation.IsInvariantForm.apply_left), and the identification with intertwiners into the dual. That identification is recorded twice: once unbundled as TauCeti.Representation.isInvariantForm_iff_isIntertwiningMap, which is the shape the proofs below use, and once as the linear equivalence TauCeti.Representation.invariantFormsEquivIntertwiningMapDual, which is the shape a dimension count of the invariant forms needs. The equivalence is not built by hand: the invariant forms are literally the invariants of linHom ρ ρ.dual (TauCeti.Representation.invariantForms_eq_invariants_linHom_dual), so it is Mathlib's Representation.invariantsEquivIntertwiningMap transported along that equality. Mathlib's Representation.invariants asks for a commutative ring and an additive group, which is why the two declarations sit in a narrower section than the rest of the file; the additive group on the space of maps V → V* is supplied explicitly, because a representation records only the additive monoid and the elaborator does not solve for a group structure inducing a given one. The equivalence is not exposed, so a downstream module uses it opaquely -- a dimension count goes through LinearEquiv.finrank_eq and never looks at a value. When a value is needed, the two simp lemmas TauCeti.Representation.invariantFormsEquivIntertwiningMapDual_apply_toLinearMap and TauCeti.Representation.invariantFormsEquivIntertwiningMapDual_symm_apply_coe are what identify it: they say the equivalence moves a form and an intertwiner to each other unchanged.

That identification is also what controls the left radical: the form is an intertwiner out of an irreducible representation, so TauCeti.Representation.IsInvariantForm.ker_eq_bot is Mathlib's Representation.IsIrreducible.injective_or_eq_zero rather than a hand-built subrepresentation argument. Schur's lemma enters through Mathlib's Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed, the same theorem that ContRepresentation.exists_eq_smul_one_of_isIrreducible rests on for a continuous representation.

References

• Character theory roadmap, Layer 7, IsInvariantForm and the invariant symmetric and alternating forms that the values +1 and -1 of the Frobenius-Schur indicator are characterized by. The indicator itself is TauCeti.Representation.frobeniusSchurIndicator; this file supplies the forms, not the count.
• J.-P. Serre, Linear Representations of Finite Groups, GTM 42 (1977), §13.2.
• I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 4.

The invariant forms of a representation

def TauCeti.Representation.IsInvariantForm {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (B : LinearMap.BilinForm k V) : Prop

A bilinear form B is invariant for a representation ρ when every ρ g preserves it: B (ρ g x) (ρ g y) = B x y; that is, when every ρ g is an isometry of B.

Equations

• TauCeti.Representation.IsInvariantForm ρ B = ∀ (g : G), TauCeti.BilinForm.IsIsometry B (ρ g)

theorem TauCeti.Representation.isInvariantForm_iff_isIsometry {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} : IsInvariantForm ρ B ↔ ∀ (g : G), BilinForm.IsIsometry B (ρ g)

A form is invariant for ρ exactly when every ρ g is an isometry of the form.

theorem TauCeti.Representation.IsInvariantForm.isIsometry {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} (hB : IsInvariantForm ρ B) (g : G) : BilinForm.IsIsometry B (ρ g)

Every element of a representation is an isometry of an invariant form.

theorem TauCeti.Representation.isInvariantForm_iff {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} : IsInvariantForm ρ B ↔ ∀ (g : G) (x y : V), (B ((ρ g) x)) ((ρ g) y) = (B x) y

A form is invariant for ρ exactly when it satisfies the pointwise equation B (ρ g x) (ρ g y) = B x y.

theorem TauCeti.Representation.IsInvariantForm.apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} (hB : IsInvariantForm ρ B) (g : G) (x y : V) : (B ((ρ g) x)) ((ρ g) y) = (B x) y

An invariant form takes the same value on ρ g x and ρ g y as it does on x and y.

def TauCeti.Representation.invariantForms {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Submodule k (LinearMap.BilinForm k V)

The invariant bilinear forms of ρ, as a submodule of all bilinear forms on V.

Equations

• TauCeti.Representation.invariantForms ρ = { carrier := {B : LinearMap.BilinForm k V | TauCeti.Representation.IsInvariantForm ρ B}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.Representation.mem_invariantForms {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} : B ∈ invariantForms ρ ↔ IsInvariantForm ρ B

Membership in TauCeti.Representation.invariantForms is invariance.

@[simp]

theorem TauCeti.Representation.isInvariantForm_zero {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} : IsInvariantForm ρ 0

The zero form is invariant.

theorem TauCeti.Representation.IsInvariantForm.add {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B C : LinearMap.BilinForm k V} (hB : IsInvariantForm ρ B) (hC : IsInvariantForm ρ C) : IsInvariantForm ρ (B + C)

A sum of invariant forms is invariant.

theorem TauCeti.Representation.IsInvariantForm.smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} (c : k) (hB : IsInvariantForm ρ B) : IsInvariantForm ρ (c • B)

A scalar multiple of an invariant form is invariant.

theorem TauCeti.Representation.IsInvariantForm.flip {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} (hB : IsInvariantForm ρ B) : IsInvariantForm ρ B.flip

Exchanging the two arguments of an invariant form leaves it invariant.

@[simp]

theorem TauCeti.Representation.isInvariantForm_trivial {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (B : LinearMap.BilinForm k V) : IsInvariantForm (Representation.trivial k G V) B

Every bilinear form is invariant for the trivial representation, which acts by the identity.

The symmetric and the alternating invariant forms

def TauCeti.Representation.symmetricInvariantForms {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Submodule k (LinearMap.BilinForm k V)

The invariant symmetric bilinear forms of ρ, as a submodule of all bilinear forms.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.Representation.alternatingInvariantForms {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Submodule k (LinearMap.BilinForm k V)

The invariant alternating bilinear forms of ρ, as a submodule of all bilinear forms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Representation.mem_symmetricInvariantForms {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} : B ∈ symmetricInvariantForms ρ ↔ IsInvariantForm ρ B ∧ B.IsSymm

Membership in TauCeti.Representation.symmetricInvariantForms is invariance together with symmetry.

@[simp]

theorem TauCeti.Representation.mem_alternatingInvariantForms {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} : B ∈ alternatingInvariantForms ρ ↔ IsInvariantForm ρ B ∧ B.IsAlt

Membership in TauCeti.Representation.alternatingInvariantForms is invariance together with alternation.

theorem TauCeti.Representation.symmetricInvariantForms_le {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : symmetricInvariantForms ρ ≤ invariantForms ρ

An invariant symmetric form is in particular invariant.

theorem TauCeti.Representation.alternatingInvariantForms_le {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : alternatingInvariantForms ρ ≤ invariantForms ρ

An invariant alternating form is in particular invariant.

theorem TauCeti.Representation.symmetricInvariantForms_inf_alternatingInvariantForms {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (h2 : IsLeftRegular 2) (ρ : Representation k G V) : symmetricInvariantForms ρ ⊓ alternatingInvariantForms ρ = ⊥

Away from characteristic two, a form cannot be both symmetric and alternating, so the two invariant subspaces meet only in 0. All that is asked of k is that 2 be regular, which over a field is IsRegular.of_ne_zero.

Invariance as intertwining with the dual representation

theorem TauCeti.Representation.IsInvariantForm.apply_left {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} (hB : IsInvariantForm ρ B) (g : G) (x y : V) : (B ((ρ g) x)) y = (B x) ((ρ g⁻¹) y)

Moving a single ρ g across an invariant form replaces it by its inverse on the other side. This is the shape invariance is used in whenever only one of the two arguments carries the action, as in the radical of the form or in a comparison with the dual representation.

theorem TauCeti.Representation.isInvariantForm_iff_isIntertwiningMap {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (B : LinearMap.BilinForm k V) : IsInvariantForm ρ B ↔ ρ.IsIntertwiningMap ρ.dual B

A bilinear form is invariant exactly when it intertwines ρ with its dual. Read as a linear map V → V*, an invariant form is a map of representations from ρ to ρ.dual, and conversely. This is what makes the invariant forms a Hom space rather than just a submodule, and it is how Schur's lemma reaches them.

theorem TauCeti.Representation.invariantForms_eq_invariants_linHom_dual {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : invariantForms ρ = (ρ.linHom ρ.dual).invariants

The invariant forms of ρ are the invariants of linHom ρ ρ.dual. Invariance of a form is intertwining of the map V → V* it is, which is Mathlib's membership criterion for the invariants of a Hom representation.

noncomputable def TauCeti.Representation.invariantFormsEquivIntertwiningMapDual {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : ↥(invariantForms ρ) ≃ₗ[k] ρ.IntertwiningMap ρ.dual

The invariant forms of ρ are the intertwiners from ρ to its dual. This is the bundled form of TauCeti.Representation.isInvariantForm_iff_isIntertwiningMap, and it is what puts the invariant forms in reach of machinery that counts intertwiners: it is Mathlib's Representation.invariantsEquivIntertwiningMap, transported along TauCeti.Representation.invariantForms_eq_invariants_linHom_dual.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Representation.invariantFormsEquivIntertwiningMapDual_apply_toLinearMap {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (B : ↥(invariantForms ρ)) : ((invariantFormsEquivIntertwiningMapDual ρ) B).toLinearMap = ↑B

The intertwiner attached to an invariant form is that form, read as a map V → V*.

@[simp]

theorem TauCeti.Representation.invariantFormsEquivIntertwiningMapDual_symm_apply_coe {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (f : ρ.IntertwiningMap ρ.dual) : ↑((invariantFormsEquivIntertwiningMapDual ρ).symm f) = f.toLinearMap

The invariant form attached to an intertwiner ρ → ρ.dual is that intertwiner, read as a bilinear form.

Invariant forms on an irreducible representation

theorem TauCeti.Representation.IsInvariantForm.ker_eq_bot {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} [ρ.IsIrreducible] (hB : IsInvariantForm ρ B) (hB0 : B ≠ 0) : LinearMap.ker B = ⊥

A nonzero invariant form on an irreducible representation has trivial left radical.

theorem TauCeti.Representation.IsInvariantForm.nondegenerate {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} [ρ.IsIrreducible] (hB : IsInvariantForm ρ B) (hB0 : B ≠ 0) : B.Nondegenerate

A nonzero invariant form on an irreducible representation is nondegenerate.

theorem TauCeti.Representation.IsInvariantForm.nondegenerate_iff_ne_zero {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} [ρ.IsIrreducible] (hB : IsInvariantForm ρ B) : B.Nondegenerate ↔ B ≠ 0

On an irreducible representation, an invariant form is nondegenerate exactly when it is nonzero. The interesting direction is TauCeti.Representation.IsInvariantForm.nondegenerate; the other is Mathlib's LinearMap.BilinForm.Nondegenerate.ne_zero, once the space an irreducible representation acts on is known to be nonzero.

theorem TauCeti.Representation.IsInvariantForm.exists_eq_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {B C : LinearMap.BilinForm k V} [FiniteDimensional k V] [IsAlgClosed k] [ρ.IsIrreducible] (hB : IsInvariantForm ρ B) (hB0 : B ≠ 0) (hC : IsInvariantForm ρ C) : ∃ (c : k), C = c • B

An invariant form on an irreducible representation is unique up to a scalar: over an algebraically closed field and in finite dimensions, every invariant form C is a scalar multiple of a nonzero invariant form B.

theorem TauCeti.Representation.IsInvariantForm.invariantForms_eq_span {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} [FiniteDimensional k V] [IsAlgClosed k] [ρ.IsIrreducible] (hB : IsInvariantForm ρ B) (hB0 : B ≠ 0) : invariantForms ρ = k ∙ B

A nonzero invariant form on an irreducible representation spans all of them: the invariant forms are a line.

theorem TauCeti.Representation.IsInvariantForm.flip_eq_or_flip_eq_neg {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} [FiniteDimensional k V] [IsAlgClosed k] [ρ.IsIrreducible] (hB : IsInvariantForm ρ B) (hB0 : B ≠ 0) : B.flip = B ∨ B.flip = -B

A nonzero invariant form on an irreducible representation is its own flip up to sign: its flip is either the form itself or its negative. This holds in every characteristic.

theorem TauCeti.Representation.IsInvariantForm.isSymm_or_isAlt {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {B : LinearMap.BilinForm k V} [FiniteDimensional k V] [IsAlgClosed k] [ρ.IsIrreducible] (h2 : 2 ≠ 0) (hB : IsInvariantForm ρ B) (hB0 : B ≠ 0) : B.IsSymm ∨ B.IsAlt

The orthogonal/symplectic dichotomy. Away from characteristic two, a nonzero invariant form on a finite-dimensional irreducible representation over an algebraically closed field is either symmetric or alternating.

theorem TauCeti.Representation.exists_isSymm_or_exists_isAlt_or_invariantForms_eq_bot {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [FiniteDimensional k V] [IsAlgClosed k] [ρ.IsIrreducible] (h2 : 2 ≠ 0) : (∃ (B : LinearMap.BilinForm k V), IsInvariantForm ρ B ∧ B ≠ 0 ∧ B.IsSymm) ∨ (∃ (B : LinearMap.BilinForm k V), IsInvariantForm ρ B ∧ B ≠ 0 ∧ B.IsAlt) ∨ invariantForms ρ = ⊥

An irreducible representation carries a symmetric, an alternating, or no invariant form. Away from characteristic two, over an algebraically closed field it carries a nonzero invariant symmetric form, or a nonzero invariant alternating form, or no nonzero invariant form at all. This is the case split the three values of the Frobenius-Schur indicator are read off from, for a finite group in TauCeti/RepresentationTheory/CharacterTable/FrobeniusSchur/Trichotomy.lean and for a compact group in TauCeti/RepresentationTheory/Compact/FrobeniusSchur/InvariantForm.lean.