Documentation

Mathlib.LinearAlgebra.FixedSubmodule

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) :

The fixed submodule of a linear map.

Equations

f.fixedSubmodule = { carrier := {x : V | f x = x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

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) :

f.fixedSubmodule ⊓ g.fixedSubmodule ≤ (f ∘ₗ g).fixedSubmodule

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) :

(f ∘ₗ g).fixedSubmodule ⊓ g.fixedSubmodule ≤ f.fixedSubmodule

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) :

↥(MulAction.stabilizer (V ≃ₗ[R] V) W) →* (V ⧸ W) ≃ₗ[R] V ⧸ W

When u : V ≃ₗ[R] V maps a submodule W into itself, this is the induced linear equivalence of V ⧸ W, as a group homomorphism.

Equations

LinearEquiv.reduce W = { toFun := fun (u : ↥(MulAction.stabilizer (V ≃ₗ[R] V) W)) => Submodule.Quotient.equiv W W ↑u ⋯, map_one' := ⋯, map_mul' := ⋯ }

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) :

((reduce W) u) (W.mkQ x) = W.mkQ (↑u x)

def LinearEquiv.fixedReduce {R : Type u_4} {V : Type u_5} [Ring R] [AddCommGroup V] [Module R V] (e : V ≃ₗ[R] V) :

(V ⧸ (↑e).fixedSubmodule) ≃ₗ[R] V ⧸ (↑e).fixedSubmodule

The linear equivalence deduced from e : V ≃ₗ[R] V by passing to the quotient by e.fixedSubmodule.

Equations

e.fixedReduce = (LinearEquiv.reduce (↑e).fixedSubmodule) ⟨e, ⋯⟩

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