The fixed submodule of a linear map #
LinearMap.fixedSubmodule: the submodule of a linear map consisting of its fixed points.
def
LinearMap.fixedSubmodule
{R : Type u_1}
[Semiring R]
{V : Type u_3}
[AddCommMonoid V]
[Module R V]
(f : V →ₗ[R] V)
:
Submodule R V
The fixed submodule of a linear map.
Instances For
@[simp]
theorem
LinearMap.mem_fixedSubmodule_iff
{R : Type u_1}
[Semiring R]
{V : Type u_3}
[AddCommMonoid V]
[Module R V]
{f : V →ₗ[R] V}
{v : V}
:
v ∈ f.fixedSubmodule ↔ f v = v
theorem
LinearMap.fixedSubmodule_eq_ker
{R : Type u_4}
[Ring R]
{V : Type u_5}
[AddCommGroup V]
[Module R V]
(f : V →ₗ[R] V)
:
f.fixedSubmodule = (f - id).ker
theorem
LinearMap.fixedSubmodule_eq_top_iff
{R : Type u_1}
[Semiring R]
{V : Type u_3}
[AddCommMonoid V]
[Module R V]
{f : V →ₗ[R] V}
:
f.fixedSubmodule = ⊤ ↔ f = id
theorem
LinearMap.fixedSubmodule_inf_fixedSubmodule_le_comp
{R : Type u_1}
[Semiring R]
{V : Type u_3}
[AddCommMonoid V]
[Module R V]
(f g : V →ₗ[R] V)
:
theorem
LinearMap.fixedSubmodule_comp_inf_fixedSubmodule_le
{R : Type u_1}
[Semiring R]
{V : Type u_3}
[AddCommMonoid V]
[Module R V]
(f g : V →ₗ[R] V)
:
theorem
LinearEquiv.fixedSubmodule_eq_top_iff
{R : Type u_1}
[Semiring R]
{V : Type u_3}
[AddCommMonoid V]
[Module R V]
{f : V ≃ₗ[R] V}
:
(↑f).fixedSubmodule = ⊤ ↔ f = refl R V
theorem
LinearEquiv.mem_stabilizer_submodule_of_le_fixedSubmodule
{R : Type u_1}
[Semiring R]
{V : Type u_3}
[AddCommMonoid V]
[Module R V]
{e : V ≃ₗ[R] V}
{W : Submodule R V}
(hW : W ≤ (↑e).fixedSubmodule)
:
e ∈ MulAction.stabilizer (V ≃ₗ[R] V) W
theorem
LinearEquiv.mem_stabilizer_fixedSubmodule
{R : Type u_1}
[Semiring R]
{V : Type u_3}
[AddCommMonoid V]
[Module R V]
(e : V ≃ₗ[R] V)
:
e ∈ MulAction.stabilizer (V ≃ₗ[R] V) (↑e).fixedSubmodule
theorem
LinearEquiv.map_eq_of_mem_fixingSubgroup
{R : Type u_1}
[Semiring R]
{V : Type u_3}
[AddCommMonoid V]
[Module R V]
(e : V ≃ₗ[R] V)
(W : Submodule R V)
(he : e ∈ fixingSubgroup (V ≃ₗ[R] V) W.carrier)
:
Submodule.map (↑e) W = W
def
LinearEquiv.reduce
{R : Type u_4}
{V : Type u_5}
[Ring R]
[AddCommGroup V]
[Module R V]
(W : Submodule R V)
:
When u : V ≃ₗ[R] V maps a submodule W into itself,
this is the induced linear equivalence of V ⧸ W, as a group homomorphism.
Instances For
@[simp]
theorem
LinearEquiv.reduce_mk
{R : Type u_4}
{V : Type u_5}
[Ring R]
[AddCommGroup V]
[Module R V]
(W : Submodule R V)
(u : ↥(MulAction.stabilizer (V ≃ₗ[R] V) W))
(x : V)
:
((reduce W) u) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (↑u x)
theorem
LinearEquiv.reduce_mkQ
{R : Type u_4}
{V : Type u_5}
[Ring R]
[AddCommGroup V]
[Module R V]
(W : Submodule R V)
(u : ↥(MulAction.stabilizer (V ≃ₗ[R] V) W))
(x : V)
:
def
LinearEquiv.fixedReduce
{R : Type u_4}
{V : Type u_5}
[Ring R]
[AddCommGroup V]
[Module R V]
(e : V ≃ₗ[R] V)
:
The linear equivalence deduced from e : V ≃ₗ[R] V
by passing to the quotient by e.fixedSubmodule.
Instances For
@[simp]
theorem
LinearEquiv.fixedReduce_mk
{R : Type u_4}
{V : Type u_5}
[Ring R]
[AddCommGroup V]
[Module R V]
(e : V ≃ₗ[R] V)
(x : V)
:
e.fixedReduce (Submodule.Quotient.mk x) = Submodule.Quotient.mk (e x)
@[simp]
theorem
LinearEquiv.fixedReduce_mkQ
{R : Type u_4}
{V : Type u_5}
[Ring R]
[AddCommGroup V]
[Module R V]
(e : V ≃ₗ[R] V)
(x : V)
:
e.fixedReduce ((↑e).fixedSubmodule.mkQ x) = (↑e).fixedSubmodule.mkQ (e x)
theorem
LinearEquiv.fixedReduce_eq_smul_iff
{R : Type u_4}
{V : Type u_5}
[Ring R]
[AddCommGroup V]
[Module R V]
(e : V ≃ₗ[R] V)
(a : R)
:
(∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x) ↔ ∀ (v : V), e v - a • v ∈ (↑e).fixedSubmodule
theorem
LinearEquiv.fixedReduce_eq_one
{R : Type u_4}
{V : Type u_5}
[Ring R]
[AddCommGroup V]
[Module R V]
(e : V ≃ₗ[R] V)
:
e.fixedReduce = refl R (V ⧸ (↑e).fixedSubmodule) ↔ ∀ (v : V), e v - v ∈ (↑e).fixedSubmodule