TriangularStabilizer.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A trace gap for positive triangular lattice stabilizers

The trace of an actual lattice stabilizer is an integer. A positive triangular stabilizer of determinant one whose trace is less than n+1 therefore has all diagonal entries equal to one. At the generic lattices used in the entropy argument it is the identity.

lemma OAI.DukePrimeDegree.sum_ge_card_of_pos_prod_one line 22
lemma OAI.DukePrimeDegree.eq_one_of_pos_prod_one_sum_card line 32
theorem OAI.DukePrimeDegree.stabilizer_trace_integral line 48
Source documentation
Actual lattice stabilizers have integral trace, by conjugating them back to the integer special linear group.
```
theorem stabilizer_trace_integral {n : ℕ} (x : X n) (g : G n)
    (hfix : rightAction x g = x) : ∃ z : ℤ, g.val.trace = z := by
…
```

theorem OAI.DukePrimeDegree.triangular_stabilizer_diagonal_eq_one line 68

Source documentation

Positivity and the integral trace gap force the diagonal to be one.

theorem triangular_stabilizer_diagonal_eq_one {n : ℕ} (x : X n) (g : G n)
    (hfix : rightAction x g = x) (htri : g.val.IsUpperTriangular)
    (hpos : ∀ i, 0 < g.val i i) (htrace : g.val.trace < n + 1) :
    ∀ i, g.val i i = 1 := by
…

theorem OAI.DukePrimeDegree.triangular_stabilizer_eq_one line 89

Source documentation

In the generic locus a positive triangular stabilizer below the first possible nonunipotent integral trace is trivial.

theorem triangular_stabilizer_eq_one {d : ℕ} (x : X (d+1))
    (hx : ∀ v ∈ pointLattice x, v ≠ 0 → ∀ j, v j ≠ 0)
    (g : G (d+1)) (hfix : rightAction x g = x)
    (htri : g.val.IsUpperTriangular) (hpos : ∀ i, 0 < g.val i i)
    (htrace : g.val.trace < (d+1 : ℕ) + 1) : g = 1 := by
…

lemma OAI.DukePrimeDegree.upperTriangular_mul_diag line 103
lemma OAI.DukePrimeDegree.specialLinear_upperTriangular_inv line 115

theorem OAI.DukePrimeDegree.exists_uniform_triangular_lift_radius line 127

Source documentation

A sufficiently small triangular lift along a positive unipotent leaf is the leaf element itself. The radius is independent of the lattice.

theorem exists_uniform_triangular_lift_radius (d : ℕ) :
    ∃ r : ℝ, 0 < r ∧ ∀ (x : X (d+1)),
      (∀ v ∈ pointLattice x, v ≠ 0 → ∀ j, v j ≠ 0) →
      ∀ (u g : G (d+1)), u.val.IsUpperTriangular → (∀ i, u.val i i = 1) →
      g ∈ matrixBall (d+1) r → g.val.IsUpperTriangular →
      rightAction x u = rightAction x g → u = g := by
…