Conjugating a monoid action by an open partial homeomorphism

Let a monoid G act on a space X and let χ : X → E be an open partial homeomorphism, for instance a chart. In the coordinates of χ, an element g acts by the conjugated map χ ∘ (g • ·) ∘ χ.symm. This file records that, near a point, conjugation is compatible with the monoid structure: the identity acts as the identity (OpenPartialHomeomorph.conj_one_smul_eventuallyEq), and a product acts as the composite of the conjugates (OpenPartialHomeomorph.conj_mul_smul_eventuallyEq). These are the local identities behind the chain-rule computation of the derivative representation at a fixed point.

OpenPartialHomeomorph.restrInvariant restricts a chart to the largest invariant open subset of its source for a finite monoid action. An equivariant chart with invariant source also has invariant target and equivariant inverse (OpenPartialHomeomorph.symm_map_smul_of_map_smul), and invariant restriction preserves equivariance (OpenPartialHomeomorph.restrInvariant_map_smul).

theorem OpenPartialHomeomorph.conj_one_smul_eventuallyEq {G : Type u_1} {X : Type u_2} {E : Type u_3} [Monoid G] [TopologicalSpace X] [TopologicalSpace E] [MulAction G X] (χ : OpenPartialHomeomorph X E) {z : E} (hz : z ∈ χ.target) : ↑χ ∘ (fun (x : X) => 1 • x) ∘ ↑χ.symm =ᶠ[nhds z] id

Near a point of the target of χ, the conjugate by χ of the action of the identity is the identity.

theorem OpenPartialHomeomorph.conj_mul_smul_eventuallyEq {G : Type u_1} {X : Type u_2} {E : Type u_3} [Monoid G] [TopologicalSpace X] [TopologicalSpace E] [MulAction G X] (χ : OpenPartialHomeomorph X E) [ContinuousConstSMul G X] {x : X} (hx : x ∈ χ.source) {h : G} (hhx : h • x ∈ χ.source) (g : G) : ↑χ ∘ (fun (x : X) => (g * h) • x) ∘ ↑χ.symm =ᶠ[nhds (↑χ x)] (↑χ ∘ (fun (x : X) => g • x) ∘ ↑χ.symm) ∘ ↑χ ∘ (fun (x : X) => h • x) ∘ ↑χ.symm

Let x be a point of the source of χ such that h • x also lies in the source. Near χ x, the conjugate by χ of the action of g * h is the composite of the conjugates of the actions of g and of h.

theorem OpenPartialHomeomorph.symm_map_smul_of_map_smul {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [TopologicalSpace E] {M : Type u_4} [SMul M X] [SMul M E] (e : OpenPartialHomeomorph X E) (hequiv : ∀ (g : M), ∀ x ∈ e.source, g • x ∈ e.source ∧ ↑e (g • x) = g • ↑e x) (g : M) (z : E) (hz : z ∈ e.target) : g • z ∈ e.target ∧ ↑e.symm (g • z) = g • ↑e.symm z

An equivariant open partial homeomorphism with invariant source has invariant target and an equivariant inverse. No continuity or monoid laws for the scalar actions are needed.

noncomputable def OpenPartialHomeomorph.restrInvariant {X : Type u_2} [TopologicalSpace X] {Y : Type u_4} [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (G : Type u_5) [Monoid G] [Finite G] [MulAction G X] [ContinuousConstSMul G X] : OpenPartialHomeomorph X Y

Restrict a chart to the largest G-invariant open subset of its source.

theorem OpenPartialHomeomorph.restrInvariant_def {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) : e.restrInvariant G = e.restrOpen (⋂ (g : G), (fun (x : X) => g • x) ⁻¹' e.source) ⋯

The invariant restriction is the open restriction to the intersection of all translates.

@[simp]

theorem OpenPartialHomeomorph.coe_restrInvariant {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) : ↑(e.restrInvariant G) = ↑e

Invariant restriction does not change the forward map.

@[simp]

theorem OpenPartialHomeomorph.coe_restrInvariant_symm {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) : ↑(e.restrInvariant G).symm = ↑e.symm

Invariant restriction does not change the inverse map.

theorem OpenPartialHomeomorph.restrInvariant_source {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) : (e.restrInvariant G).source = e.source ∩ ⋂ (g : G), (fun (x : X) => g • x) ⁻¹' e.source

The source of the invariant restriction is the source intersected with all its translates.

theorem OpenPartialHomeomorph.restrInvariant_source_subset {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) : (e.restrInvariant G).source ⊆ e.source

The invariant restriction has source contained in the original source.

@[simp]

theorem OpenPartialHomeomorph.restrInvariant_target {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) : (e.restrInvariant G).target = e.target ∩ ↑e.symm ⁻¹' ⋂ (g : G), (fun (x : X) => g • x) ⁻¹' e.source

The target of the invariant restriction consists of points whose inverse image has its whole orbit in the original source.

theorem OpenPartialHomeomorph.restrInvariant_target_subset {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) : (e.restrInvariant G).target ⊆ e.target

The invariant restriction has target contained in the original target.

@[simp]

theorem OpenPartialHomeomorph.mem_restrInvariant_source_iff {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) {x : X} : x ∈ (e.restrInvariant G).source ↔ ∀ (g : G), g • x ∈ e.source

A point belongs to the invariant restriction exactly when its whole orbit is in the source.

theorem OpenPartialHomeomorph.mem_restrInvariant_source_of_forall_smul_eq {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) {x : X} (hx : ∀ (g : G), g • x = x) (hxe : x ∈ e.source) : x ∈ (e.restrInvariant G).source

A common fixed point in the original source belongs to the invariant restriction.

theorem OpenPartialHomeomorph.smul_mem_restrInvariant_source {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ (e.restrInvariant G).source) (g : G) : g • x ∈ (e.restrInvariant G).source

The source of an invariant restriction is invariant.

theorem OpenPartialHomeomorph.restrInvariant_map_smul {G : Type u_1} {X : Type u_2} [Monoid G] [TopologicalSpace X] [MulAction G X] {Y : Type u_4} [TopologicalSpace Y] [Finite G] [ContinuousConstSMul G X] [SMul G Y] {e : OpenPartialHomeomorph X Y} (hf : ∀ (g : G), ∀ x ∈ e.source, ↑e (g • x) = g • ↑e x) {x : X} (hx : x ∈ (e.restrInvariant G).source) (g : G) : g • x ∈ (e.restrInvariant G).source ∧ ↑(e.restrInvariant G) (g • x) = g • ↑(e.restrInvariant G) x

A chart that is equivariant on its source stays equivariant after invariant restriction, whose source is invariant.