Functoriality of Lipschitz groups

A ring homomorphism of Clifford algebras that sends vector generators to vector generators restricts to a homomorphism of Lipschitz groups. In particular, a quadratic isometry induces such a homomorphism, and its action on vectors is natural with respect to that isometry.

Main results

• CliffordAlgebra.lipschitzGroupMapOf restricts a generator-preserving Clifford ring homomorphism to the Lipschitz groups.
• QuadraticMap.Isometry.lipschitzGroupMap is the homomorphism induced on Lipschitz groups.
• QuadraticMap.IsometryEquiv.lipschitzGroupEquiv is the equivalence induced on Lipschitz groups.
• QuadraticMap.Isometry.map_lipschitzVectorAction proves naturality of the Lipschitz action.
• QuadraticMap.IsometryEquiv.orthogonalGroupCongr_lipschitzToOrthogonal packages that result as an equality of orthogonal-group homomorphisms.

theorem CliffordAlgebra.map_mem_lipschitzGroup_of_map_ι {R : Type u} [CommRing R] {S : Type v} [CommRing S] {M : Type w} [AddCommGroup M] [Module R M] {N : Type x} [AddCommGroup N] [Module S N] {Q : QuadraticForm R M} {Q' : QuadraticForm S N} (F : CliffordAlgebra Q →+* CliffordAlgebra Q') (f : M → N) (hF : ∀ (m : M), F ((ι Q) m) = (ι Q') (f m)) {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzGroup Q) : (Units.map ↑F) x ∈ lipschitzGroup Q'

A Clifford ring homomorphism that sends vectors to vectors preserves the Lipschitz group.

def CliffordAlgebra.lipschitzGroupMapOf {R : Type u} [CommRing R] {S : Type v} [CommRing S] {M : Type w} [AddCommGroup M] [Module R M] {N : Type x} [AddCommGroup N] [Module S N] {Q : QuadraticForm R M} {Q' : QuadraticForm S N} (F : CliffordAlgebra Q →+* CliffordAlgebra Q') (f : M → N) (hF : ∀ (m : M), F ((ι Q) m) = (ι Q') (f m)) : ↥(lipschitzGroup Q) →* ↥(lipschitzGroup Q')

Restrict a generator-preserving Clifford ring homomorphism to the Lipschitz groups.

Equations

• CliffordAlgebra.lipschitzGroupMapOf F f hF = { toFun := fun (x : ↥(lipschitzGroup Q)) => ⟨(Units.map ↑F) ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CliffordAlgebra.coe_lipschitzGroupMapOf_apply {R : Type u} [CommRing R] {S : Type v} [CommRing S] {M : Type w} [AddCommGroup M] [Module R M] {N : Type x} [AddCommGroup N] [Module S N] {Q : QuadraticForm R M} {Q' : QuadraticForm S N} (F : CliffordAlgebra Q →+* CliffordAlgebra Q') (f : M → N) (hF : ∀ (m : M), F ((ι Q) m) = (ι Q') (f m)) (x : ↥(lipschitzGroup Q)) : ↑↑((lipschitzGroupMapOf F f hF) x) = F ↑↑x

The Clifford value of the restricted Lipschitz-group map is the original ring homomorphism.

theorem CliffordAlgebra.lipschitzGroupMapOf_inv_coe {R : Type u} [CommRing R] {S : Type v} [CommRing S] {M : Type w} [AddCommGroup M] [Module R M] {N : Type x} [AddCommGroup N] [Module S N] {Q : QuadraticForm R M} {Q' : QuadraticForm S N} (F : CliffordAlgebra Q →+* CliffordAlgebra Q') (f : M → N) (hF : ∀ (m : M), F ((ι Q) m) = (ι Q') (f m)) (x : ↥(lipschitzGroup Q)) : F ↑(↑x)⁻¹ = ↑(↑((lipschitzGroupMapOf F f hF) x))⁻¹

Mapping the inverse of a Lipschitz unit agrees with taking the inverse after restriction.

theorem QuadraticMap.Isometry.map_mem_lipschitzGroup {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) {x : (CliffordAlgebra Q₁)ˣ} (hx : x ∈ lipschitzGroup Q₁) : (Units.map ↑(CliffordAlgebra.map f).toRingHom) x ∈ lipschitzGroup Q₂

Mapping Clifford units along a quadratic isometry preserves the Lipschitz group.

def QuadraticMap.Isometry.lipschitzGroupMap {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) : ↥(lipschitzGroup Q₁) →* ↥(lipschitzGroup Q₂)

The Clifford map of a quadratic isometry restricts to a homomorphism of Lipschitz groups.

Equations

• f.lipschitzGroupMap = CliffordAlgebra.lipschitzGroupMapOf (CliffordAlgebra.map f).toRingHom ⇑f ⋯

@[simp]

theorem QuadraticMap.Isometry.coe_lipschitzGroupMap_apply {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (x : ↥(lipschitzGroup Q₁)) : ↑↑(f.lipschitzGroupMap x) = (CliffordAlgebra.map f) ↑↑x

Coercing the induced Lipschitz-group map is the corresponding Clifford-algebra map.

@[simp]

theorem QuadraticMap.Isometry.map_lipschitzGroup_inv_coe {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (x : ↥(lipschitzGroup Q₁)) : (CliffordAlgebra.map f) ↑(↑x)⁻¹ = ↑(↑(f.lipschitzGroupMap x))⁻¹

Mapping the inverse of a Lipschitz unit agrees with taking the inverse after mapping.

@[simp]

theorem QuadraticMap.Isometry.lipschitzGroupMap_id {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] (Q₁ : QuadraticForm R M₁) : (id Q₁).lipschitzGroupMap = MonoidHom.id ↥(lipschitzGroup Q₁)

The identity isometry induces the identity homomorphism of a Lipschitz group.

@[simp]

theorem QuadraticMap.Isometry.lipschitzGroupMap_comp {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {M₃ : Type x} [AddCommGroup M₃] [Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} (f : Q₂ →qᵢ Q₃) (g : Q₁ →qᵢ Q₂) : f.lipschitzGroupMap.comp g.lipschitzGroupMap = (f.comp g).lipschitzGroupMap

Lipschitz-group maps respect composition of quadratic isometries.

@[simp]

theorem QuadraticMap.Isometry.map_lipschitzVectorAction {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} [Invertible 2] (f : Q₁ →qᵢ Q₂) (x : ↥(lipschitzGroup Q₁)) (m : M₁) : f ((CliffordAlgebra.lipschitzVectorAction Q₁ x) m) = (CliffordAlgebra.lipschitzVectorAction Q₂ (f.lipschitzGroupMap x)) (f m)

The Lipschitz action commutes with the map induced by a quadratic isometry.

def QuadraticMap.IsometryEquiv.lipschitzGroupEquiv {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) : ↥(lipschitzGroup Q₁) ≃* ↥(lipschitzGroup Q₂)

The equivalence of Lipschitz groups induced by a quadratic isometry equivalence.

Equations

• e.lipschitzGroupEquiv = e.toIsometry.lipschitzGroupMap.toMulEquiv e.symm.toIsometry.lipschitzGroupMap ⋯ ⋯

@[simp]

theorem QuadraticMap.IsometryEquiv.lipschitzGroupEquiv_apply {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) (x : ↥(lipschitzGroup Q₁)) : e.lipschitzGroupEquiv x = e.toIsometry.lipschitzGroupMap x

The equivalence induced on Lipschitz groups agrees with the forward isometry map.

@[simp]

theorem QuadraticMap.IsometryEquiv.lipschitzGroupEquiv_symm {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) : e.lipschitzGroupEquiv.symm = e.symm.lipschitzGroupEquiv

The inverse of the induced Lipschitz equivalence is induced by the inverse quadratic isometry.

@[simp]

theorem QuadraticMap.IsometryEquiv.orthogonalGroupCongr_lipschitzToOrthogonal {R : Type u} [CommRing R] {M₁ : Type v} [AddCommGroup M₁] [Module R M₁] {M₂ : Type w} [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} [Invertible 2] (e : IsometryEquiv Q₁ Q₂) (x : ↥(lipschitzGroup Q₁)) : e.orthogonalGroupCongr ((CliffordAlgebra.lipschitzToOrthogonal Q₁) x) = (CliffordAlgebra.lipschitzToOrthogonal Q₂) (e.lipschitzGroupEquiv x)

The Lipschitz action is natural under a quadratic isometry equivalence.