BoundaryInverseShadow.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Transporting two compact shadows through a coarse inverse

theorem OAI.PolycyclicRecognition.factor_quotient_action_second line 16

Source documentation

On the second factor, the quotient action is the Cartan action.

theorem factor_quotient_action_second
    {N D G Q : Type*} [Group N] [Group D] [Group G] [Group Q]
    (ι : N →* G) (κ : D →* G) (π : N →* Q)
    (α : D →* MulAut Q) (act : G →* Equiv.Perm Q)
    (hact : ∀ u d q, act (ι u * κ d) q = π u * α d q) (d : D) (q : Q) :
    act (κ d) q = α d q := by
…

theorem OAI.PolycyclicRecognition.compact_lift_boundary_shadow line 26

Source documentation

A continuous section turns a compact quotient shadow into compact ambient representatives of that same shadow.

theorem compact_lift_boundary_shadow
    {G S T : Type*} [Group G] [TopologicalSpace G]
    [One S] [One T] [TopologicalSpace T]
    (actS : G →* Equiv.Perm S) (actT : G →* Equiv.Perm T)
    (B : S → T) (f : G → G)
    (σ : T → G) (hσ : Continuous σ) (hsection : ∀ q, actT (σ q) 1 = q)
    (K : Set T) (hK : IsCompact K)
    (hshadow : ∀ x, ∃ q ∈ K, B (actS x 1) = actT (f x) q) :
    ∃ C : Set G, IsCompact C ∧ ∀ x, ∃ u ∈ C,
      B (actS x 1) = actT (f x) (actT u 1) := by
…

theorem OAI.PolycyclicRecognition.inverse_boundary_compact_shadow line 44

Source documentation

Compose the forward and inverse boundary shadows. Compact group representatives of the shadows and the coarse-inverse estimate put their composition in one fixed compact source shadow.

theorem inverse_boundary_compact_shadow
    {G S T : Type*} [Group G] [MetricSpace G] [IsTopologicalGroup G]
    [IsIsometricSMul G G] [ProperSpace G] [One S] [One T]
    (actS : G →* Equiv.Perm S) (actT : G →* Equiv.Perm T)
    (B : S → T) (C : T → S) (f g : G → G)
    {L error E : ℝ} (hL : 0 ≤ L)
    (hg : ∀ x y, dist (g x) (g y) ≤ L * dist x y + error)
    (hinv : ∀ x, dist (g (f x)) x ≤ E)
    (KT KS : Set G) (hKT : IsCompact KT) (hKS : IsCompact KS)
    (hB : ∀ x, ∃ u ∈ KT, B (actS x 1) = actT (f x) (actT u 1))
    (hC : ∀ y, ∃ v ∈ KS, C (actT y 1) = actS (g y) (actS v 1)) :
    ∃ K : Set G, IsCompact K ∧ ∀ x, ∃ k ∈ K,
…

theorem OAI.PolycyclicRecognition.boundary_left_inverse_of_compact_shadow line 98

Source documentation

A composition constrained by one compact source shadow is the identity when the negative ray fixes the basepoint and contracts compact shadows. The compact-shadow premise is supplied by the coarse-inverse transport theorem above.

theorem boundary_left_inverse_of_compact_shadow
    {G S T : Type*} [Group G] [TopologicalSpace G]
    [One S] [TopologicalSpace S] [T2Space S]
    (act : G →* Equiv.Perm S) (hact : ∀ g, Continuous (act g))
    (B : S → T) (C : T → S) (ray : ℕ → G)
    (hfix : ∀ n, act (ray n) 1 = 1)
    (hcontract : ∀ K : Set G, IsCompact K → ∀ k : ℕ → G,
      (∀ n, k n ∈ K) → Tendsto (fun n => act (ray n) (act (k n) 1)) atTop (𝓝 1))
    (hshadow : ∃ K : Set G, IsCompact K ∧ ∀ x, ∃ k ∈ K,
      C (B (act x 1)) = act x (act k 1)) :
    ∀ x, C (B (act x 1)) = act x 1 := by
…