Mathlib.LinearAlgebra.AffineSpace.Dimension

(Finite) Dimension of an affine subspace #

This file defines the dimension of an affine subspace to be ⊥ for the empty subspace, and otherwise equal to the Module.rank of the direction of the subspace. The finite dimension is similary defined using Module.finrank.

Main definitions #

AffineSubspace.dim: Dimension expressed as WithBot Cardinal
AffineSubspace.finDim: Dimension expressed as WithBot ℕ with a junk value of 0 for infinite dimensional spaces.

source

noncomputable def AffineSubspace.dim {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] (s : AffineSubspace R A) :

WithBot Cardinal.{v}

The dimension of s is equal to ⊥ if s = ⊥, and otherwise it is equal to the dimension of s interpreted as a linear space.

Equations

s.dim = if s = ⊥ then ⊥ else ↑(Module.rank R ↥s.direction)

Instances For

source

noncomputable def AffineSubspace.finDim {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] (s : AffineSubspace R A) :

WithBot ℕ

The dimension of s is equal to ⊥ if s = ⊥, and otherwise it is equal to the finite dimension of s interpreted as a linear space. Note that this inherits Module.finranks junk value: AffineSubspace.finDim s = 0 for infinite dimensional subspaces.

Equations

s.finDim = WithBot.map (⇑Cardinal.toNat) s.dim

Instances For

source

@[simp]

theorem AffineSubspace.dim_bot {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] :

⊥.dim = ⊥

source

@[simp]

theorem AffineSubspace.finDim_bot {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] :

⊥.finDim = ⊥

source

@[simp]

theorem AffineSubspace.dim_singleton {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] [Nontrivial R] (x : A) :

{x}.dim = 0

source

@[simp]

theorem AffineSubspace.finDim_singleton {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] [Nontrivial R] (x : A) :

{x}.finDim = 0

source

@[simp]

theorem AffineSubspace.dim_eq_bot_iff {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} :

s.dim = ⊥ ↔ s = ⊥

source

@[simp]

theorem AffineSubspace.finDim_eq_bot_iff {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} :

s.finDim = ⊥ ↔ s = ⊥

source

theorem AffineSubspace.dim_ne_bot_iff {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} :

s.dim ≠ ⊥ ↔ (↑s).Nonempty

source

theorem AffineSubspace.finDim_ne_bot_iff {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} :

s.finDim ≠ ⊥ ↔ (↑s).Nonempty

source

theorem AffineSubspace.dim_eq_rank {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} (h : s ≠ ⊥) :

s.dim = ↑(Module.rank R ↥s.direction)

source

theorem AffineSubspace.finDim_eq_finrank {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} (h : s ≠ ⊥) :

s.finDim = ↑(Module.finrank R ↥s.direction)

source

@[simp]

theorem AffineSubspace.dim_toAffineSubspace {R : Type u} {V : Type v} [AddCommGroup V] [Ring R] [Module R V] (s : Submodule R V) :

(↑s).dim = ↑(Module.rank R ↥s)

source

@[simp]

theorem AffineSubspace.finDim_toAffineSubspace {R : Type u} {V : Type v} [AddCommGroup V] [Ring R] [Module R V] (s : Submodule R V) :

(↑s).finDim = ↑(Module.finrank R ↥s)

source

@[simp]

theorem AffineSubspace.finDim_eq_finrank_of_not_finite {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} [Module.Free R ↥s.direction] [StrongRankCondition R] (h : ¬Module.Finite R ↥s.direction) :

s.finDim = 0

source

@[simp]

theorem AffineSubspace.dim_lt_aleph0 {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] [StrongRankCondition R] (s : AffineSubspace R A) [Module.Finite R ↥s.direction] :

s.dim < ↑Cardinal.aleph0

source

theorem AffineSubspace.finite_iff_dim_lt_aleph0 {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] [StrongRankCondition R] (s : AffineSubspace R A) [Module.Free R ↥s.direction] :

Module.Finite R ↥s.direction ↔ s.dim < ↑Cardinal.aleph0

source

theorem AffineSubspace.finite_of_finDim_ne_zero {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] [StrongRankCondition R] (s : AffineSubspace R A) [Module.Free R ↥s.direction] (h : s.finDim ≠ 0) :

Module.Finite R ↥s.direction

source

theorem AffineSubspace.finDim_eq_map_dim_toNat {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} :

s.finDim = WithBot.map (⇑Cardinal.toNat) s.dim

source

theorem AffineSubspace.dim_eq_finDim_unbot {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} (hs : s ≠ ⊥) [StrongRankCondition R] [Module.Finite R ↥s.direction] :

s.dim = ↑(s.finDim.unbot ⋯)

source

theorem AffineSubspace.dim_mono {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s t : AffineSubspace R A} (h : s ≤ t) :

s.dim ≤ t.dim

source

theorem AffineSubspace.finDim_mono {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s t : AffineSubspace R A} [StrongRankCondition R] [Module.Finite R ↥t.direction] (h : s ≤ t) :

s.finDim ≤ t.finDim

source

theorem AffineSubspace.lift_dim_map_le {R : Type u} {V : Type v} {V' : Type v'} {A : Type a} {A' : Type a'} [AddCommGroup V] [AddTorsor V A] [AddCommGroup V'] [AddTorsor V' A'] [Ring R] [Module R V] [Module R V'] (f : A →ᵃ[R] A') (s : AffineSubspace R A) :

WithBot.map Cardinal.lift.{v, v'} (map f s).dim ≤ WithBot.map Cardinal.lift.{v', v} s.dim

source

theorem AffineSubspace.dim_map_le {R : Type u} {V : Type v} {A A₁ : Type a} [AddCommGroup V] [AddTorsor V A] [AddTorsor V A₁] [Ring R] [Module R V] (f : A →ᵃ[R] A₁) (s : AffineSubspace R A) :

(map f s).dim ≤ s.dim

source

theorem AffineSubspace.finDim_map_le_finDim {R : Type u} {V : Type v} {V' : Type v'} {A : Type a} {A' : Type a'} [AddCommGroup V] [AddTorsor V A] [AddCommGroup V'] [AddTorsor V' A'] [Ring R] [Module R V] [Module R V'] [StrongRankCondition R] (f : A →ᵃ[R] A') (s : AffineSubspace R A) [Module.Finite R ↥s.direction] :

(map f s).finDim ≤ s.finDim

source

theorem AffineSubspace.lift_dim_map_of_injective {R : Type u} {V : Type v} {V' : Type v'} {A : Type a} {A' : Type a'} [AddCommGroup V] [AddTorsor V A] [AddCommGroup V'] [AddTorsor V' A'] [Ring R] [Module R V] [Module R V'] {f : A →ᵃ[R] A'} (hf : Function.Injective ⇑f) (s : AffineSubspace R A) :

WithBot.map Cardinal.lift.{v, v'} (map f s).dim = WithBot.map Cardinal.lift.{v', v} s.dim

source

theorem AffineSubspace.dim_map_of_injective {R : Type u} {V : Type v} {A A₁ : Type a} [AddCommGroup V] [AddTorsor V A] [AddTorsor V A₁] [Ring R] [Module R V] {f : A →ᵃ[R] A₁} (hf : Function.Injective ⇑f) (s : AffineSubspace R A) :

(map f s).dim = s.dim

source

theorem AffineSubspace.finDim_map_of_injective {R : Type u} {V : Type v} {V' : Type v'} {A : Type a} {A' : Type a'} [AddCommGroup V] [AddTorsor V A] [AddCommGroup V'] [AddTorsor V' A'] [Ring R] [Module R V] [Module R V'] {f : A →ᵃ[R] A'} (hf : Function.Injective ⇑f) (s : AffineSubspace R A) :

(map f s).finDim = s.finDim

source

@[simp]

theorem AffineSubspace.dim_le_zero_iff_subsingleton {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} [IsDomain R] [Module.IsTorsionFree R ↥s.direction] :

s.dim ≤ 0 ↔ (↑s).Subsingleton

source

@[simp]

theorem AffineSubspace.finDim_le_zero_iff_subsingleton {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [Ring R] [Module R V] {s : AffineSubspace R A} [StrongRankCondition R] [IsDomain R] [Module.IsTorsionFree R ↥s.direction] [Module.Finite R ↥s.direction] :

s.finDim ≤ 0 ↔ (↑s).Subsingleton

source

theorem AffineSubspace.finDim_strictMono {R : Type u} {V : Type v} {A : Type a} [AddCommGroup V] [AddTorsor V A] [DivisionRing R] [Module R V] {s t : AffineSubspace R A} [Module.Finite R ↥t.direction] (h : s < t) :

s.finDim < t.finDim