Skip to content

Commit 3792095

Browse files
AntoineChambert-Loirpre-commit-ci-lite[bot]ocfnash
committed
feat(LinearAlgebra/Transvection): characterization of transvections among dilatransvections (#33348)
* `LinearEquiv.fixedReduce`. Pass a linear equivalence to the quotient by a fixed subspace. * Characterize transvections among dilatransvections by the fact that their reduction is the identity. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
1 parent 88d1cd4 commit 3792095

File tree

6 files changed

+316
-9
lines changed

6 files changed

+316
-9
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4816,6 +4816,7 @@ public import Mathlib.LinearAlgebra.Finsupp.Span
48164816
public import Mathlib.LinearAlgebra.Finsupp.SumProd
48174817
public import Mathlib.LinearAlgebra.Finsupp.Supported
48184818
public import Mathlib.LinearAlgebra.Finsupp.VectorSpace
4819+
public import Mathlib.LinearAlgebra.FixedSubmodule
48194820
public import Mathlib.LinearAlgebra.FreeAlgebra
48204821
public import Mathlib.LinearAlgebra.FreeModule.Basic
48214822
public import Mathlib.LinearAlgebra.FreeModule.Determinant

‎Mathlib/Algebra/Module/Submodule/Pointwise.lean‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -201,6 +201,9 @@ protected def pointwiseDistribMulAction : DistribMulAction α (Submodule R M) wh
201201

202202
scoped[Pointwise] attribute [instance] Submodule.pointwiseDistribMulAction
203203

204+
theorem pointwise_smul_def {a : α} {S : Submodule R M} :
205+
a • S = S.map (DistribSMul.toLinearMap R M a) := rfl
206+
204207
open Pointwise
205208

206209
@[simp, norm_cast]
@@ -563,4 +566,24 @@ lemma sup_set_smul (s t : Set S) :
563566

564567
end set_acting_on_submodules
565568

569+
section group
570+
571+
variable {R G M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
572+
[Group G] [DistribMulAction G M] [SMulCommClass G R M]
573+
{S : Submodule R M}
574+
575+
open MulAction
576+
577+
lemma stabilizer_coe :
578+
stabilizer G S = stabilizer G (S : Set M) := by
579+
ext
580+
rw [mem_stabilizer_iff, SetLike.ext'_iff, coe_pointwise_smul,
581+
← mem_stabilizer_iff]
582+
583+
theorem mem_stabilizer_submodule_iff_map_eq {e : G} :
584+
e ∈ stabilizer G S ↔ S.map (DistribSMul.toLinearMap R M e) = S := by
585+
rfl
586+
587+
end group
588+
566589
end Submodule

‎Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,25 @@ theorem isCompl_iff_disjoint [FiniteDimensional K V] (s t : Submodule K V)
8686
IsCompl s t ↔ Disjoint s t :=
8787
⟨fun h ↦ h.1, fun h ↦ ⟨h, codisjoint_iff.mpr <| eq_top_of_disjoint s t hdim h⟩⟩
8888

89+
theorem sup_span_singleton_eq_top_iff [Module.Finite K V] {W : Submodule K V} {v : V} (hv : v ∉ W) :
90+
W ⊔ span K {v} = ⊤ ↔ finrank K (V ⧸ W) = 1 := by
91+
refine ⟨fun hW ↦ ?_, fun hW ↦ ?_⟩
92+
· suffices W ⊓ span K {v} = ⊥ by
93+
have hv₀ : v ≠ 0 := by aesop
94+
have aux := finrank_sup_add_finrank_inf_eq W (span K {v})
95+
rw [hW, finrank_span_singleton hv₀, this, finrank_bot, finrank_top,
96+
← finrank_quotient_add_finrank W] at aux
97+
lia
98+
refine (Submodule.eq_bot_iff _).mpr fun w hw ↦ ?_
99+
obtain ⟨ht, t, rfl⟩ : w ∈ W ∧ ∃ t : K, t • v = w := by simpa [mem_span_singleton] using hw
100+
rcases eq_or_ne t 0 with rfl | ht₀; · simp
101+
rw [Submodule.smul_mem_iff _ ht₀] at ht
102+
contradiction
103+
· apply Submodule.eq_top_of_disjoint
104+
· rw [← W.finrank_quotient_add_finrank, add_comm, add_le_add_iff_left, hW]
105+
aesop
106+
· exact Submodule.disjoint_span_singleton_of_notMem hv
107+
89108
end DivisionRing
90109

91110
end Submodule

‎Mathlib/LinearAlgebra/FixedSubmodule.lean‎

Lines changed: 163 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,163 @@
1+
/-
2+
Copyright (c) 2026 Antoine Chambert-Loir. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Antoine Chambert-Loir
5+
-/
6+
7+
module
8+
9+
public import Mathlib.Algebra.Module.Submodule.Pointwise
10+
public import Mathlib.GroupTheory.GroupAction.FixingSubgroup
11+
public import Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
12+
public import Mathlib.GroupTheory.GroupAction.Ring
13+
public import Mathlib.LinearAlgebra.DFinsupp
14+
public import Mathlib.LinearAlgebra.Quotient.Basic
15+
16+
/-!
17+
# The fixed submodule of a linear map
18+
19+
- `LinearMap.fixedSubmodule`: the submodule of a linear map consisting of its fixed points.
20+
21+
-/
22+
23+
@[expose] public section
24+
25+
namespace LinearMap
26+
27+
open Pointwise Submodule MulAction
28+
29+
variable {R : Type*} [Semiring R]
30+
{U V : Type*} [AddCommMonoid U] [AddCommMonoid V]
31+
[Module R U] [Module R V] (e : V ≃ₗ[R] V)
32+
33+
34+
/-- The fixed submodule of a linear map. -/
35+
def fixedSubmodule (f : V →ₗ[R] V) : Submodule R V where
36+
carrier := { x | f x = x }
37+
add_mem' {x y} hx hy := by aesop
38+
zero_mem' := by simp
39+
smul_mem' r x hx := by aesop
40+
41+
@[simp]
42+
theorem mem_fixedSubmodule_iff {f : V →ₗ[R] V} {v : V} :
43+
v ∈ f.fixedSubmodule ↔ f v = v := by
44+
simp [fixedSubmodule]
45+
46+
theorem fixedSubmodule_eq_ker {R : Type*} [Ring R]
47+
{V : Type*} [AddCommGroup V] [Module R V] (f : V →ₗ[R] V) :
48+
f.fixedSubmodule = LinearMap.ker (f - id (R := R)) := by
49+
ext; simp [sub_eq_zero]
50+
51+
theorem fixedSubmodule_eq_top_iff {f : V →ₗ[R] V} :
52+
f.fixedSubmodule = ⊤ ↔ f = id (R := R) := by
53+
simp [LinearMap.ext_iff, Submodule.ext_iff]
54+
55+
theorem fixedSubmodule_inf_fixedSubmodule_le_comp (f g : V →ₗ[R] V) :
56+
f.fixedSubmodule ⊓ g.fixedSubmodule ≤ (f ∘ₗ g).fixedSubmodule := by
57+
intro; simp_all
58+
59+
theorem fixedSubmodule_comp_inf_fixedSubmodule_le (f g : V →ₗ[R] V) :
60+
(f ∘ₗ g).fixedSubmodule ⊓ g.fixedSubmodule ≤ f.fixedSubmodule := by intro; aesop
61+
62+
end LinearMap
63+
64+
namespace LinearEquiv
65+
66+
open Pointwise LinearMap Submodule MulAction
67+
68+
variable {R : Type*} [Semiring R]
69+
{U V : Type*} [AddCommMonoid U] [AddCommMonoid V]
70+
[Module R U] [Module R V] (e : V ≃ₗ[R] V)
71+
72+
variable {P : Submodule R U} {Q : Submodule R V}
73+
74+
theorem fixedSubmodule_eq_top_iff {f : V ≃ₗ[R] V} :
75+
f.fixedSubmodule = ⊤ ↔ f = .refl R V := by
76+
simp [LinearEquiv.ext_iff, Submodule.ext_iff]
77+
78+
theorem mem_stabilizer_submodule_of_le_fixedSubmodule
79+
{e : V ≃ₗ[R] V} {W : Submodule R V} (hW : W ≤ LinearMap.fixedSubmodule e) :
80+
e ∈ stabilizer (V ≃ₗ[R] V) W := by
81+
rw [mem_stabilizer_submodule_iff_map_eq]
82+
apply le_antisymm
83+
· rintro _ ⟨x, hx : x ∈ W, rfl⟩
84+
suffices e x = x by simpa [this, coe_coe]
85+
rw [← coe_toLinearMap, ← mem_fixedSubmodule_iff]
86+
exact hW hx
87+
· intro x hx
88+
refine ⟨x, hx, ?_⟩
89+
simp only [DistribSMul.toLinearMap_apply, LinearEquiv.smul_def]
90+
rw [← coe_toLinearMap, ← mem_fixedSubmodule_iff]
91+
exact hW hx
92+
93+
theorem mem_stabilizer_fixedSubmodule (e : V ≃ₗ[R] V) :
94+
e ∈ stabilizer _ e.fixedSubmodule :=
95+
mem_stabilizer_submodule_of_le_fixedSubmodule (le_refl _)
96+
97+
theorem map_eq_of_mem_fixingSubgroup (W : Submodule R V)
98+
(he : e ∈ fixingSubgroup _ W.carrier) :
99+
map e.toLinearMap W = W := by
100+
ext v
101+
simp only [mem_fixingSubgroup_iff, carrier_eq_coe, SetLike.mem_coe, LinearEquiv.smul_def] at he
102+
refine ⟨fun ⟨w, hv, hv'⟩ ↦ ?_, fun hv ↦ ?_⟩
103+
· simp only [SetLike.mem_coe, coe_coe] at hv hv'
104+
rwa [← hv', he w hv]
105+
· refine ⟨v, hv, he v hv⟩
106+
107+
open Pointwise MulAction
108+
109+
variable {R V : Type*} [Ring R] [AddCommGroup V] [Module R V]
110+
111+
/-- When `u : V ≃ₗ[R] V` maps a submodule `W` into itself,
112+
this is the induced linear equivalence of `V ⧸ W`, as a group homomorphism. -/
113+
def reduce (W : Submodule R V) : stabilizer (V ≃ₗ[R] V) W →* (V ⧸ W) ≃ₗ[R] (V ⧸ W) where
114+
toFun u := Quotient.equiv W W u.val u.prop
115+
map_mul' u v := by
116+
ext x
117+
obtain ⟨y, rfl⟩ := W.mkQ_surjective x
118+
simp
119+
map_one' := by aesop
120+
121+
@[simp]
122+
theorem reduce_mk (W : Submodule R V) (u : stabilizer (V ≃ₗ[R] V) W) (x : V) :
123+
reduce W u (Submodule.Quotient.mk x) = Submodule.Quotient.mk (u.val x) :=
124+
rfl
125+
126+
theorem reduce_mkQ (W : Submodule R V) (u : stabilizer (V ≃ₗ[R] V) W) (x : V) :
127+
reduce W u (W.mkQ x) = W.mkQ (u.val x) :=
128+
rfl
129+
130+
/-- The linear equivalence deduced from `e : V ≃ₗ[R] V`
131+
by passing to the quotient by `e.fixedSubmodule`. -/
132+
def fixedReduce (e : V ≃ₗ[R] V) :
133+
(V ⧸ e.fixedSubmodule) ≃ₗ[R] V ⧸ e.fixedSubmodule :=
134+
reduce e.fixedSubmodule ⟨e, e.mem_stabilizer_fixedSubmodule⟩
135+
136+
@[simp]
137+
theorem fixedReduce_mk (e : V ≃ₗ[R] V) (x : V) :
138+
fixedReduce e (Submodule.Quotient.mk x) = Submodule.Quotient.mk (e x) :=
139+
rfl
140+
141+
@[simp]
142+
theorem fixedReduce_mkQ (e : V ≃ₗ[R] V) (x : V) :
143+
fixedReduce e (e.fixedSubmodule.mkQ x) = e.fixedSubmodule.mkQ (e x) :=
144+
rfl
145+
146+
theorem fixedReduce_eq_smul_iff (e : V ≃ₗ[R] V) (a : R) :
147+
(∀ x, e.fixedReduce x = a • x) ↔
148+
∀ v, e v - a • v ∈ e.fixedSubmodule := by
149+
simp only [← e.fixedSubmodule.ker_mkQ, mem_ker, map_sub, ← fixedReduce_mkQ, sub_eq_zero]
150+
constructor
151+
· intro H x; simp [H]
152+
· intro H x
153+
have ⟨y, hy⟩ := e.fixedSubmodule.mkQ_surjective x
154+
rw [← hy]
155+
apply H
156+
157+
theorem fixedReduce_eq_one (e : V ≃ₗ[R] V) :
158+
e.fixedReduce = LinearEquiv.refl R _ ↔ ∀ v, e v - v ∈ e.fixedSubmodule := by
159+
simpa [LinearEquiv.ext_iff] using fixedReduce_eq_smul_iff e 1
160+
161+
end LinearEquiv
162+
163+
end

0 commit comments

Comments
 (0)