(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.

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)

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

@[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 = ⊥

@[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 = ⊥

@[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

@[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

@[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 = ⊥

@[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 = ⊥

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

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

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)

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)

@[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)

@[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)

@[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

@[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

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

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

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

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

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

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

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

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

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

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

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

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

@[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

@[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

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