Documentation

TauCeti.Algebra.Bialgebra.GroupLike.Lift

Extending homomorphisms of group-like elements #

When group-like elements form a basis of a bialgebra over a commutative semiring, every monoid homomorphism from its group-like elements extends uniquely to a bialgebra homomorphism. Over a domain, linear independence follows from torsion-freeness by linearIndep_groupLikeVal. Only the source needs the basis hypotheses. This is the coordinate-algebra extension step in descent of morphisms between groups of multiplicative type.

The construction uses TauCeti.GroupLike.evaluationBialgEquivOfLinearIndependentOfSpanEqTop and Mathlib's MonoidAlgebra.mapDomainBialgHom. See Milne, Algebraic Groups (2017), §12.

source
noncomputable def MonoidHom.liftBialgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] (f : GroupLike R A →* GroupLike R B) (hlinear : LinearIndependent R GroupLike.val) (hA : Submodule.span R (Set.range GroupLike.val) = ⊤) :
A →ₐc[R] B

Extend a homomorphism of group-like elements across a group-like spanning basis. No linear independence or spanning assumption is imposed on the target.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MonoidHom.liftBialgHom_apply_val {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] (f : GroupLike R A →* GroupLike R B) (hlinear : LinearIndependent R GroupLike.val) (hA : Submodule.span R (Set.range GroupLike.val) = ⊤) (x : GroupLike R A) :
    (f.liftBialgHom hlinear hA) ↑x = ↑(f x)

    The extension agrees with the prescribed homomorphism on group-like elements.

    source
    @[simp]
    theorem MonoidHom.groupLikeMap_liftBialgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] (f : GroupLike R A →* GroupLike R B) (hlinear : LinearIndependent R GroupLike.val) (hA : Submodule.span R (Set.range GroupLike.val) = ⊤) :
    TauCeti.GroupLike.map (f.liftBialgHom hlinear hA) = f

    Restricting the extension to group-like elements recovers the given homomorphism.

    source
    theorem MonoidHom.liftBialgHom_unique {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] (f : GroupLike R A →* GroupLike R B) (hlinear : LinearIndependent R GroupLike.val) (hA : Submodule.span R (Set.range GroupLike.val) = ⊤) (g : A →ₐc[R] B) (hg : ∀ (x : GroupLike R A), g ↑x = ↑(f x)) :
    g = f.liftBialgHom hlinear hA

    A bialgebra morphism extending the prescribed group-like homomorphism is unique.