Rank of a diagonal family

Lax342547.DirectRanks · concepts/Lax342547/DirectRanks.lean · lax-342547

proven

Loading review…

Natural Language Statement

Lemma

The range of a coordinatewise linear map is the product of its coordinate ranges, so its rank is the sum of their ranks.

Concept map

2 concepts

100%

Proven claimThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

lem✓Lax342547.DirectRanks

⊢Lax342547Proofs.DirectRanks.diagonal_rank_sum

Lean source view on GitHub

Show types on hover

1	import Lax342547.RestrictionRank
2	import Mathlib.LinearAlgebra.Pi
3
4	/-!
5	---
6	title: Rank of a diagonal family
7	type: lemma
8	---
9	The range of a coordinatewise linear map is the product of its coordinate ranges, so its rank is the sum of their ranks.
10	-/
11
12	namespace Lax342547.DirectRanks
13
14	open scoped BigOperators
15
16	noncomputable def rangeProductEquiv {K ι : Type} [Field K]
17	{V W : ι → Type} [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
18	[∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
19	(M : ∀ i, V i →ₗ[K] W i) :
20	LinearMap.range (LinearMap.piMap M) ≃ₗ[K] (∀ i, LinearMap.range (M i)) := by
21	classical
22	let f : LinearMap.range (LinearMap.piMap M) →ₗ[K] (∀ i, LinearMap.range (M i)) :=
23	{ toFun := fun w i => ⟨w.val i,by obtain ⟨v,hv⟩ := w.property; exact ⟨v i,congrFun hv i⟩⟩
24	map_add' := by intros; rfl
25	map_smul' := by intros; rfl }
26	refine LinearEquiv.ofBijective f ?_
27	constructor
28	· intro w z h
29	apply Subtype.ext
30	funext i
31	exact congrArg Subtype.val (congrFun h i)
32	· intro w
33	have hex : ∀ i, ∃ v, M i v = (w i).val := fun i => (w i).property
34	choose v hv using hex
35	refine ⟨⟨fun i => (w i).val,⟨v,?_⟩⟩,?_⟩
36	· funext i
37	exact hv i
38	· rfl
39
40	axiom diagonal_rank_sum {K ι : Type} [Field K] [Fintype ι]
41	{V W : ι → Type} [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
42	[∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
43	[∀ i, FiniteDimensional K (W i)] (M : ∀ i, V i →ₗ[K] W i) :
44	Module.finrank K (LinearMap.range (LinearMap.piMap M)) =
45	∑ i, Module.finrank K (LinearMap.range (M i))
46
47	end Lax342547.DirectRanks
48