LinearMap.bijective_or_eq_zero
theorem LinearMap.bijective_or_eq_zero :
∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
[inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsSimpleModule R M] [inst_6 : IsSimpleModule R N]
(f : M →ₗ[R] N), Function.Bijective ⇑f ∨ f = 0
**Schur's Lemma** for linear maps between (possibly distinct) simple modules states that for any ring `R` and two simple `R`-modules `M` and `N`, any linear map `f` from `M` to `N` is either bijective or the zero map. Here, a module is considered simple if it has only two submodules, `⊥` and `⊤`. A function is called bijective if it is both injective (each element of the range corresponds to exactly one element of the domain) and surjective (all elements in the range are covered).
More concisely: For any ring `R` and simple `R`-modules `M` and `N`, any linear map `f` from `M` to `N` is either a bijection or the zero map.
|
LinearMap.bijective_of_ne_zero
theorem LinearMap.bijective_of_ne_zero :
∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
[inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsSimpleModule R M] [inst_6 : IsSimpleModule R N]
{f : M →ₗ[R] N}, f ≠ 0 → Function.Bijective ⇑f
The theorem `LinearMap.bijective_of_ne_zero` states that for any ring `R`, and any two simple `R`-modules `M` and `N`, any non-zero linear map `f : M →ₗ[R] N` is bijective. Here, a simple `R`-module is a module that only has two submodules: the zero submodule and the module itself. A bijective function is one that is both injective (no two different inputs map to the same output) and surjective (every possible output is mapped by some input).
More concisely: If `R` is a ring and `M` and `N` are simple `R`-modules, then any non-zero linear map from `M` to `N` is a bijection.
|