QuotientNeighborhoods.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Small relative lifts on the arithmetic quotient

Open quotient charts provide a neighborhood in which any two points are related by a matrix in a prescribed identity neighborhood. This is the local lifting step used with compactly controlled centralizer returns.

lemma OAI.DukePrimeDegree.rightOrbitMap_isOpen line 21

theorem OAI.DukePrimeDegree.exists_open_small_relative_lifts line 32

Source documentation

Any identity neighborhood gives a quotient neighborhood with small relative lifts between all of its points.

theorem exists_open_small_relative_lifts {n : ℕ}
    (x : X n) (W : Set (G n)) (hW : W ∈ 𝓝 1) :
    ∃ V : Set (X n), IsOpen V ∧ x ∈ V ∧
      ∀ y ∈ V, ∀ z ∈ V, ∃ g ∈ W, rightAction y g = z := by
…

theorem OAI.DukePrimeDegree.exists_open_matrix_relative_lifts line 47

Source documentation

The matrix-ball form needed for exceptional returns.

theorem exists_open_matrix_relative_lifts {n : ℕ} (x : X n) {r : ℝ} (hr : 0 < r) :
    ∃ V : Set (X n), IsOpen V ∧ x ∈ V ∧
      ∀ y ∈ V, ∀ z ∈ V, ∃ g ∈ matrixBall n r, rightAction y g = z :=
…

def OAI.DukePrimeDegree.rightSubgroupAction line 53
Source documentation
Right translations are a left action of the opposite subgroup.
```
@[instance_reducible] def rightSubgroupAction {n : ℕ} (C : Subgroup (G n)) :
    MulAction (MulOpposite C) (X n) where
…
```
lemma OAI.DukePrimeDegree.rightSubgroupAction_continuous line 62