Finite Bochner linearization #
Let a finite group G act on a space X, and let Ο be a continuous linear representation of
G on a topological vector space F over a ring π in which the order of G is invertible.
The Bochner average of a map c : X β F is
bochnerAverage Ο c y = |G|β»ΒΉ β’ β g, Ο gβ»ΒΉ (c (g β’ y)).
It is always G-equivariant: bochnerAverage Ο c (h β’ y) = Ο h (bochnerAverage Ο c y). It is
the nonlinear analogue of the averaging of a linear map used in Maschke's theorem
(LinearMap.equivariantProjection), and it fixes maps that are already equivariant.
When the derivative of each y β¦ c (g β’ y) at a point is Ο g β Dβ, for a fixed linear map
Dβ, the Bochner average also has derivative Dβ there. This is the situation at a fixed point
x of the action when c is a chart centred at x and Ο is the derivative representation of
G at x in that chart: the average then has derivative the identity at x, and the inverse
function theorem turns it into a chart around x in which G acts linearly through Ο. This is
Bochner's linearization theorem for finite groups, the local model of a smooth orbifold around a
point with finite isotropy. No faithfulness of the action is assumed.
The chart is constructed for an action on an arbitrary topological space X equipped with an
E-valued open partial homeomorphism Ο around the fixed point, with differentiability
expressed for the conjugated maps Ο β (g β’ Β·) β Ο.symm; for X = E one may take Ο to be the
identity.
Main definitions #
ContRepresentation.bochnerAverage Ο c: the Bochner average ofc : X β Fwith respect toΟ.TauCeti.isotropyRepresentation: the derivative representation ofGat a fixed point, in the coordinates of a chart.
The Bochner chart (Ο.trans Ξ).restrInvariant G composes Ο with a chart Ξ of the
Bochner average and restricts to the largest G-invariant open subset of its domain.
Main results #
ContRepresentation.bochnerAverage_smul: the Bochner average is equivariant.ContRepresentation.bochnerAverage_eq_self: averaging an equivariant map does not change it.ContRepresentation.bochnerAverage_apply_of_forall_smul_eq: at a fixed point the Bochner average isRepresentation.averageMapapplied to the value ofc.ContRepresentation.hasStrictFDerivAt_bochnerAverage_comp_of_intertwining: the derivative of the Bochner average when the derivatives ofc (g β’ Β·)intertwine withΟ.ContRepresentation.contDiffOn_bochnerAverage_comp: the Bochner average is as smooth as the mapsc (g β’ Β·);OpenPartialHomeomorph.contDiffOn_bochnerChart_comp_symmis the corresponding statement for the Bochner chart, andOpenPartialHomeomorph.contDiffAt_comp_bochnerChart_symmthe one for its inverse.OpenPartialHomeomorph.smul_mem_restrInvariant_source,OpenPartialHomeomorph.map_mem_bochnerChart_target: the Bochner chart has aG-invariant domain and aΟ-invariant target.OpenPartialHomeomorph.bochnerChart_smul,OpenPartialHomeomorph.bochnerChart_symm_map: the Bochner chart and its inverse intertwine the action ofGwithΟ.OpenPartialHomeomorph.exists_equivariant_chart: Bochner linearization. Near a fixed point of a finite group action whose conjugated maps have strict derivativesΟ gfor a representationΟ, there is a chart withG-invariant domain, centred at the point, with derivative the identity, in whichgacts asΟ g.OpenPartialHomeomorph.map_eq_one_iff_mem_germKernel: the derivative representation detects the ineffective kernel. An element ofGlies in the germ kernel at the fixed point, that is, acts as the identity near it, exactly when its derivative there is the identity.OpenPartialHomeomorph.exists_target_eq_sumOfConjugatesInnerSublevel: overβ, in finite dimensions, a chart in whichGacts linearly restricts, inside any neighbourhood of a point it sends to0, to an equivariant chart onto an invariant ball of an averaged inner product (Representation.sumOfConjugatesInnerSublevel), with invariant preconnected domain.
References #
- S. Bochner, Compact groups of differentiable transformations, Ann. of Math. (2) 46 (1945), 372β381.
- I. Moerdijk and D. A. Pronk, Orbifolds, sheaves and groupoids, K-Theory 12 (1997), 3β21, where this linearization gives the local charts of a proper Γ©tale groupoid.
- A. Adem, J. Leida and Y. Ruan, Orbifolds and Stringy Topology, Cambridge Tracts in Mathematics 171, Cambridge University Press, 2007, Ch. 1, for linear local models of orbifolds, including nonfaithful ones and their ineffective kernel.
The Bochner average |G|β»ΒΉ β’ β g, Ο gβ»ΒΉ (c (g β’ y)) of a map c : X β F with respect to a
continuous representation Ο of a finite group G acting on X. It is G-equivariant
(ContRepresentation.bochnerAverage_smul).
Instances For
The Bochner average is G-equivariant.
Averaging a map that is already G-equivariant does not change it.
At a point fixed by G, the Bochner average is the average of the value of c over the
representation, that is, its image under Representation.averageMap. In particular it lies in the
invariants of Ο.
The Bochner average along a map f : Y β X, as a function of the point of Y.
The Bochner average along f : Y β X is continuous on s if each w β¦ c (g β’ f w) is.
The Bochner average along f : Y β X is continuous if each w β¦ c (g β’ f w) is.
The strict derivative of the Bochner average along a map f : E β X, given the strict
derivatives D g of the maps w β¦ c (g β’ f w).
The derivative of the Bochner average along a map f : E β X, given the derivatives D g of
the maps w β¦ c (g β’ f w).
If the strict derivative of each w β¦ c (g β’ f w) at z is Ο g β Dβ, then the Bochner
average along f has strict derivative Dβ at z.
If the derivative of each w β¦ c (g β’ f w) at z is Ο g β Dβ, then the Bochner average
along f has derivative Dβ at z.
The Bochner average along f : E β X is C^n at z if each w β¦ c (g β’ f w) is.
The Bochner average along f : E β X is C^n on s if each w β¦ c (g β’ f w) is.
On its domain, the Bochner chart is the Bochner average.
The Bochner chart intertwines the action of G with Ο.
The target of the Bochner chart is invariant under Ο.
The inverse of the Bochner chart intertwines Ο with the action of G.
In the coordinates of Ο, the Bochner chart has strict derivative D at the base point.
In the coordinates of Ο, the Bochner chart is C^n on any set where the maps
w β¦ c (g β’ Ο.symm w) are, intersected with the domain of the chart.
In the coordinates of Ο, the inverse of the Bochner chart is C^n at a point w of its
target, provided that, in the coordinates of Ο, the Bochner average is C^n with an invertible
derivative at the point corresponding to w.
The isotropy representation of G at a fixed point x, in the coordinates of a chart Ο
around x: g acts by the derivative at Ο x of the conjugated map Ο β (g β’ Β·) β Ο.symm.
Multiplicativity is the chain rule at the fixed point.
Instances For
If each conjugated map Ο β (g β’ Β·) β Ο.symm has a strict derivative at Ο x, then this
strict derivative is given by the isotropy representation.
Bochner linearization for a finite group. Let G act on X fixing x, let Ο be an
E-valued chart around x, and suppose that each conjugated map Ο β (g β’ Β·) β Ο.symm has strict
derivative Ο g at Ο x, where Ο is a continuous representation of G on E. Then there is a
chart e around x with G-invariant domain inside that of Ο, sending x to 0, with
derivative the identity at x in the coordinates of Ο, in which g acts linearly as Ο g.
The chart is the Bochner chart of y β¦ Ο y - Ο x. When the conjugated maps are strictly
differentiable at Ο x, one can take Ο to be TauCeti.isotropyRepresentation
(TauCeti.hasStrictFDerivAt_conj_smul_isotropyRepresentation).
The derivative representation detects the ineffective kernel. In the setting of
OpenPartialHomeomorph.exists_equivariant_chart, an element of G acts as the identity near the
fixed point x, that is, lies in the germ kernel TauCeti.MulAction.germKernel G x, exactly when
its derivative Ο g at x, in the coordinates of Ο, is the identity.
Shrinking an equivariant chart to an invariant ball. Let e be a chart centred at x,
with G-invariant domain, in which G acts linearly through a representation Ο on a
finite-dimensional real inner product space. Inside any neighbourhood s of x, the chart e
restricts to a chart e' onto a positive strict sublevel set of the orbit-sum inner product of
Ο, an open convex Ο-invariant neighbourhood of 0. The restriction e' has the same
underlying map as e, and its domain is G-invariant and preconnected.