ConeQuotientRestriction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Transporting the first quotient restriction to a tile's frame

theorem OAI.PolycyclicRecognition.quotient_lift_coordinate line 16

Source documentation

The quotient orbit point is independent of the chosen overlapping factorization of the ambient element.

theorem quotient_lift_coordinate
    (ι : N →* G) (κ : D →* G) (π : N →* Q)
    (α : D →* MulAut Q) (act : G →* Equiv.Perm Q)
    (hact : ∀ n d q, act (ι n * κ d) q = π n * α d q)
    (n : N) (d : D) : act (ι n * κ d) 1 = π n := by
…

theorem OAI.PolycyclicRecognition.quotient_restriction_in_anchor_frame line 25

Source documentation

A first-sheet quotient bound becomes a translated automorphic image in the second-sheet frame. The translation may have arbitrary size.

theorem quotient_restriction_in_anchor_frame
    (ι : N →* G) (κ : D →* G) (π : N →* Q)
    (α : D →* MulAut Q) (act : G →* Equiv.Perm Q)
    (hact : ∀ n d q, act (ι n * κ d) q = π n * α d q)
    (base anchor endpoint : G) (u n₀ : N) (d d₀ : D)
    (hlift : anchor⁻¹ * endpoint = ι u * κ d)
    (hframe : anchor⁻¹ * base = ι n₀ * κ d₀)
    (T : Set Q) (hfirst : act (base⁻¹ * endpoint) 1 ∈ T) :
    π u ∈ π n₀ • (α d₀ '' T) := by
…