Points and spanned hyperplanes

3 fully proved1 ready to prove

Hyperplanes spanned by point sets

DefinitionAffine hyperplanes in \(\mathbb{R}^d\)#✓fully proved

An affine subspace \(A\) of \(\mathbb{R}^d\) is an affine hyperplane when there are a nonzero linear functional \(\ell \colon \mathbb{R}^d \to \mathbb{R}\) and a real number \(c\) such that \(A = \{x \in \mathbb{R}^d : \ell(x) = c\}\).

def IsAffineHyperplane (d : ℕ) (Hp : AffineSubspace ℝ (Fin d → ℝ)) : Prop :=
  ∃ (l : (Fin d → ℝ) →ₗ[ℝ] ℝ) (c : ℝ), l ≠ 0 ∧ ∀ x, x ∈ Hp ↔ l x = c

Sources

• OWR-1183-011.

Used by 1

Used byHyperplanes spanned by a point set

DefinitionHyperplanes spanned by a point set#✓fully proved

For a set \(P \subseteq \mathbb{R}^d\), the hyperplanes spanned by \(P\) are the affine hyperplanes of \(\mathbb{R}^d\) that equal the affine span of some subset of \(P\).

def SpannedHyperplaneSet (d : ℕ) (P : Set (Fin d → ℝ)) :
    Set (AffineSubspace ℝ (Fin d → ℝ)) :=
  {Hp | IsAffineHyperplane d Hp ∧ ∃ Q : Set (Fin d → ℝ), Q ⊆ P ∧ affineSpan ℝ Q = Hp}

Sources

• OWR-1183-011.

Uses 1 · Used by 1

Statement usesAffine hyperplanes in \(\mathbb{R}^d\)

Used byInjective point-to-hyperplane matching question

DefinitionInjective point-to-hyperplane matching question#✓fully proved

The statement that for every \(d \ge 1\) and every set \(P \subseteq \mathbb{R}^d\) whose affine span is all of \(\mathbb{R}^d\), writing \(\mathcal{H}\) for the set of affine hyperplanes of \(\mathbb{R}^d\) that equal the affine span of some subset of \(P\), there is an injective map \(f \colon P \to \mathcal{H}\) with \(p \in f(p)\) for every \(p \in P\).

def OWR1183Question : Prop :=
  ∀ (d : ℕ) (_hd : 1 ≤ d) (P : Set (Fin d → ℝ)), affineSpan ℝ P = ⊤ →
    ∃ f : P → ↥(SpannedHyperplaneSet d P),
      Function.Injective f ∧ ∀ p : P, p.val ∈ (f p).val

Sources

• the question of OWR-1183-011.

Uses 1 · Used by 1

Statement usesHyperplanes spanned by a point set

Used bySpanning point sets have injective point-to-hyperplane matchings

Injective point-to-hyperplane matchings

TheoremSpanning point sets have injective point-to-hyperplane matchings#●ready to prove

For every \(d \ge 1\) and every set \(P \subseteq \mathbb{R}^d\) whose affine span is all of \(\mathbb{R}^d\), let \(\mathcal{H}\) be the set of affine hyperplanes of \(\mathbb{R}^d\) that equal the affine span of some subset of \(P\). Then there is an injective map \(f \colon P \to \mathcal{H}\) with \(p \in f(p)\) for every \(p \in P\).

This answers the question of OWR-1183-011 affirmatively. It follows from Farley's Theorem 11: every geometric lattice of finite rank greater than \(1\), of any cardinality, has an injective map sending each atom to a coatom containing it; apply it to the lattice of affine flats spanned by subsets of \(P\).

public theorem_wanted OWR1183Question_holds : ITSP.OWR1183Question

Sources

• J. D. Farley, A question of Björner from 1981: infinite geometric lattices of finite rank have matchings, Australasian Journal of Combinatorics 82 (2022) 228-235, arXiv:2004.11972, https://arxiv.org/abs/2004.11972.

Uses 1

Statement usesInjective point-to-hyperplane matching question

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.