Functoriality in the coordinate Hopf algebra

TauCeti.Algebra.AlgebraicGroup.FunctorOfPoints gives the convolution group on WithConv (H →ₐ[R] A), functorial in the value algebra A. This file adds the other variance needed for the functor-of-points dictionary: a bialgebra morphism φ : H₁ →ₐc[R] H₂ induces, by pre-composition, a monoid homomorphism WithConv (H₂ →ₐ[R] A) →* WithConv (H₁ →ₐ[R] A).

For a commutative Hopf algebra H, this is the contravariant functoriality of A ↦ Hom_R(H, A) in the coordinate Hopf algebra. It is one of the formal pieces needed by the reductive-groups roadmap Layer 0 target "R-points as a group" and its follow-up "the functor of points" dictionary.

Main declarations

• AlgHom.mapDomain: pre-composition by a bialgebra morphism as a monoid homomorphism of convolution monoids.
• AlgHom.mapDomain_id and AlgHom.mapDomain_comp: identity and composition laws.
• AlgHom.mapDomainMulEquiv: the equiv-version of AlgHom.mapDomain, turning a bialgebra isomorphism into a multiplicative equivalence of convolution monoids.
• AlgHom.mapValue_mapDomain: pre-composition in the coordinate algebra commutes with post-composition in the value algebra.
• AlgHom.mapDomain_inv_apply: pointwise inverse formula after pre-composition.

The convolution-preservation proof is the bialgebra-morphism version of Mathlib's AlgHom.convMul_comp_bialgHom_distrib, from Mathlib.RingTheory.Bialgebra.Convolution.

noncomputable def TauCeti.AlgHom.mapDomain {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommSemiring A] [Algebra R A] (φ : H₁ →ₐc[R] H₂) : WithConv (H₂ →ₐ[R] A) →* WithConv (H₁ →ₐ[R] A)

Contravariant functoriality of convolution algebra homomorphisms in the source bialgebra. A bialgebra morphism φ : H₁ →ₐc[R] H₂ sends an A-valued point of H₂ to an A-valued point of H₁ by pre-composition.

Equations

• TauCeti.AlgHom.mapDomain φ = { toFun := fun (f : WithConv (H₂ →ₐ[R] A)) => WithConv.toConv (f.ofConv.comp ↑φ), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.AlgHom.mapDomain_apply {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommSemiring A] [Algebra R A] (φ : H₁ →ₐc[R] H₂) (f : WithConv (H₂ →ₐ[R] A)) : (mapDomain φ) f = WithConv.toConv (f.ofConv.comp ↑φ)

mapDomain φ acts pointwise by pre-composition with φ.

theorem TauCeti.AlgHom.mapDomain_apply_apply {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommSemiring A] [Algebra R A] (φ : H₁ →ₐc[R] H₂) (f : WithConv (H₂ →ₐ[R] A)) (h : H₁) : ((mapDomain φ) f).ofConv h = f.ofConv (φ h)

Pointwise form of mapDomain_apply.

@[simp]

theorem TauCeti.AlgHom.mapDomain_id {R : Type u_1} {H₁ : Type u_2} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Bialgebra R H₁] [CommSemiring A] [Algebra R A] : mapDomain (BialgHom.id R H₁) = MonoidHom.id (WithConv (H₁ →ₐ[R] A))

Pre-composition by the identity bialgebra morphism is the identity map on the convolution monoid.

theorem TauCeti.AlgHom.mapDomain_comp {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {H₃ : Type u_4} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Semiring H₃] [Bialgebra R H₁] [Bialgebra R H₂] [Bialgebra R H₃] [CommSemiring A] [Algebra R A] (ψ : H₂ →ₐc[R] H₃) (φ : H₁ →ₐc[R] H₂) : mapDomain (ψ.comp φ) = (mapDomain φ).comp (mapDomain ψ)

Pre-composition by a composite bialgebra morphism is the composite of the corresponding pre-composition maps.

noncomputable def TauCeti.AlgHom.mapDomainMulEquiv {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommSemiring A] [Algebra R A] (e : H₁ ≃ₐc[R] H₂) : WithConv (H₂ →ₐ[R] A) ≃* WithConv (H₁ →ₐ[R] A)

A bialgebra isomorphism e : H₁ ≃ₐc[R] H₂ induces a multiplicative equivalence of the convolution monoids of points, by pre-composition: the equiv-version of the contravariant functoriality mapDomain.

Equations

• TauCeti.AlgHom.mapDomainMulEquiv e = { toFun := ⇑(TauCeti.AlgHom.mapDomain ↑e), invFun := ⇑(TauCeti.AlgHom.mapDomain ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.AlgHom.mapDomainMulEquiv_apply {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommSemiring A] [Algebra R A] (e : H₁ ≃ₐc[R] H₂) (f : WithConv (H₂ →ₐ[R] A)) : (mapDomainMulEquiv e) f = (mapDomain ↑e) f

mapDomainMulEquiv acts by the underlying mapDomain in the forward direction.

@[simp]

theorem TauCeti.AlgHom.mapDomainMulEquiv_symm_apply {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommSemiring A] [Algebra R A] (e : H₁ ≃ₐc[R] H₂) (f : WithConv (H₁ →ₐ[R] A)) : (mapDomainMulEquiv e).symm f = (mapDomain ↑e.symm) f

mapDomainMulEquiv acts by pre-composition with the inverse bialgebra equivalence in the reverse direction.

theorem TauCeti.AlgHom.mapValue_mapDomain {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_5} {B : Type u_6} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (φ : H₁ →ₐc[R] H₂) (χ : A →ₐ[R] B) : (mapDomain φ).comp (mapValue χ) = (mapValue χ).comp (mapDomain φ)

Pre-composition in the coordinate bialgebra commutes with post-composition in the value algebra.

theorem TauCeti.AlgHom.mapDomain_inv_apply {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {A : Type u_5} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [HopfAlgebra R H₂] [CommSemiring A] [Algebra R A] (φ : H₁ →ₐc[R] H₂) (f : WithConv (H₂ →ₐ[R] A)) (h : H₁) : ((mapDomain φ) f⁻¹).ofConv h = f.ofConv ((HopfAlgebraStruct.antipode R) (φ h))

The inverse in the target convolution group is transported by mapDomain pointwise as pre-composition with the bialgebra morphism. The group homomorphism statement follows from mapDomain being a MonoidHom; this lemma records the concrete formula used at points.