Convolution product on bialgebra homs #

This file constructs the ring structure on algebra homs C → A where C is a bialgebra and A an algebra, and also the ring structure on bialgebra homs C → A where C and A are bialgebras. Both multiplications are given by

         .
        / \
f * g = f g
        \ /
         .

source

noncomputable instance AlgHom.instOne_toric {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] :

One (C →ₐ[R] A)

Equations

AlgHom.instOne_toric = { one := (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R C) }

source

noncomputable instance AlgHom.instMul_toric {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] :

Mul (C →ₐ[R] A)

Equations

AlgHom.instMul_toric = { mul := fun (f g : C →ₐ[R] A) => (Algebra.TensorProduct.lmul' R).comp ((Algebra.TensorProduct.map f g).comp (Bialgebra.comulAlgHom R C)) }

source

noncomputable instance AlgHom.instPowNat_toric {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] :

Pow (C →ₐ[R] A) ℕ

Equations

AlgHom.instPowNat_toric = { pow := fun (f : C →ₐ[R] A) (n : ℕ) => npowRec n f }

source

theorem AlgHom.one_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] :

1 = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R C)

source

theorem AlgHom.mul_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (f g : C →ₐ[R] A) :

f * g = (Algebra.TensorProduct.lmul' R).comp ((Algebra.TensorProduct.map f g).comp (Bialgebra.comulAlgHom R C))

source

theorem AlgHom.pow_succ {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (f : C →ₐ[R] A) (n : ℕ) :

f ^ (n + 1) = f ^ n * f

source

@[simp]

theorem AlgHom.one_apply' {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (c : C) :

1 c = (algebraMap R A) (CoalgebraStruct.counit c)

source

theorem AlgHom.toLinearMap_one {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] :

↑1 = 1

source

theorem AlgHom.toLinearMap_mul {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (f g : C →ₐ[R] A) :

(f * g).toLinearMap = f.toLinearMap * g.toLinearMap

source

theorem AlgHom.toLinearMap_pow {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] (f : C →ₐ[R] A) (n : ℕ) :

(f ^ n).toLinearMap = f.toLinearMap ^ n

source

theorem AlgHom.mul_distrib_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Semiring C] [Bialgebra R C] [Algebra R A] [Bialgebra R B] (f g : C →ₐ[R] A) (h : B →ₐc[R] C) :

(f * g).comp ↑h = f.comp ↑h * g.comp ↑h

source

theorem AlgHom.comp_mul_distrib {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Semiring C] [Bialgebra R C] [Algebra R A] [Algebra R B] (f g : C →ₐ[R] A) (h : A →ₐ[R] B) :

h.comp (f * g) = h.comp f * h.comp g

source

noncomputable instance AlgHom.instMonoid_toric {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] :

Monoid (C →ₐ[R] A)

Equations

AlgHom.instMonoid_toric = Function.Injective.monoid AlgHom.toLinearMap ⋯ ⋯ ⋯ ⋯

source

noncomputable instance AlgHom.instCommMonoid_toric {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring C] [Bialgebra R C] [Algebra R A] [Coalgebra.IsCocomm R C] :

CommMonoid (C →ₐ[R] A)

Equations

AlgHom.instCommMonoid_toric = Function.Injective.commMonoid AlgHom.toLinearMap ⋯ ⋯ ⋯ ⋯

source

noncomputable instance BialgHom.instOne_toric {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] :

One (C →ₐc[R] A)

Equations

BialgHom.instOne_toric = { one := (Bialgebra.unitBialgHom R A).comp (Bialgebra.counitBialgHom R C) }

source

theorem BialgHom.one_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] :

1 = (Bialgebra.unitBialgHom R A).comp (Bialgebra.counitBialgHom R C)

source

@[simp]

theorem BialgHom.one_apply' {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] (c : C) :

1 c = (algebraMap R A) (CoalgebraStruct.counit c)

source

theorem BialgHom.toLinearMap_one {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] :

(toCoalgHom 1).toLinearMap = 1

source

noncomputable instance BialgHom.instMul_toric {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] :

Mul (C →ₐc[R] A)

Equations

BialgHom.instMul_toric = { mul := fun (f g : C →ₐc[R] A) => (Bialgebra.mulBialgHom R A).comp ((Bialgebra.TensorProduct.map f g).comp (Bialgebra.comulBialgHom R C)) }

source

noncomputable instance BialgHom.instPowNat_toric {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] :

Pow (C →ₐc[R] A) ℕ

Equations

BialgHom.instPowNat_toric = { pow := fun (f : C →ₐc[R] A) (n : ℕ) => npowRec n f }

source

theorem BialgHom.mul_def {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] (f g : C →ₐc[R] A) :

f * g = (Bialgebra.mulBialgHom R A).comp ((Bialgebra.TensorProduct.map f g).comp (Bialgebra.comulBialgHom R C))

source

theorem BialgHom.pow_succ {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] (f : C →ₐc[R] A) (n : ℕ) :

f ^ (n + 1) = f ^ n * f

source

theorem BialgHom.toLinearMap_mul {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] (f g : C →ₐc[R] A) :

(f * g).toLinearMap = f.toLinearMap * g.toLinearMap

source

theorem BialgHom.toLinearMap_pow {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] (f : C →ₐc[R] A) (n : ℕ) :

(f ^ n).toLinearMap = f.toLinearMap ^ n

source

noncomputable instance BialgHom.instCommMonoid_toric {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [CommSemiring A] [CommSemiring C] [Bialgebra R A] [Bialgebra R C] [Coalgebra.IsCocomm R C] :

CommMonoid (C →ₐc[R] A)

Equations

BialgHom.instCommMonoid_toric = Function.Injective.commMonoid (fun (x : C →ₐc[R] A) => ↑x) ⋯ ⋯ ⋯ ⋯

Documentation

Toric.Mathlib.RingTheory.Bialgebra.Convolution

Convolution product on bialgebra homs #