FiniteLinearSymmetries.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finiteness of linear height symmetries

The finite-symmetry step used in Lemma support-symmetries reduces to permuting a finite spanning collection of covectors. The elementary linear algebra fact proved here applies equally to vectors in the dual height space. It does not assume that the permutation of covectors determines a symmetry: it proves uniqueness from the spanning hypothesis.

theorem OAI.PolycyclicRecognition.finite_linear_symmetries line 22
Source documentation
There are only finitely many invertible continuous linear maps preserving a fixed finite spanning collection of vectors.
```
theorem finite_linear_symmetries (s : Finset W)
    (hspan : Submodule.span ℝ (s : Set W) = ⊤) :
    Set.Finite {A : W ≃L[ℝ] W | ∀ w ∈ s, A w ∈ s} := by
…
```
theorem OAI.PolycyclicRecognition.finite_range_of_preserves_spanning_finset line 42
Source documentation
A family preserving the same finite spanning set has finitely many linear parts, supplying the finiteness hypothesis of the height homomorphism theorem.
```
theorem finite_range_of_preserves_spanning_finset {H : Type*}
    (A : H → W ≃L[ℝ] W) (s : Finset W)
    (hspan : Submodule.span ℝ (s : Set W) = ⊤)
    (hpreserve : ∀ h w, w ∈ s → A h w ∈ s) :
    Set.Finite (Set.range A) := by
…
```