Bilinear map coming from two linear maps

Stream: Is there code for X?

[Kevin Buzzard]

I couldn't find this. Do we have it?

import Mathlib.RingTheory.Coalgebra
import Mathlib.Algebra.Algebra.Bilinear

universe u v w x

variable {R : Type u} [CommSemiring R]
variable {A : Type v} [AddCommMonoid A] [Module R A]
variable {B : Type w} [AddCommMonoid B] [Module R B]
variable (S : Type x) [Semiring S] [Algebra R S]

def do_we_have_this (φ : A →ₗ[R] S) (ψ : B →ₗ[R] S) : A →ₗ[R] B →ₗ[R] S where
  toFun a := {
    toFun := fun b ↦ φ a * ψ b
    map_add' := by simp [mul_add]
    map_smul' := by simp
  }
  map_add' a₁ a₂ := by ext; simp [add_mul]
  map_smul' r a := by ext; simp

The multiplication on S is used in the definition of the map, which made it different to the things I could find.

[Adam Topaz]

We must have the multiplication map out of the tensor product of S with itself, so you can tensor phi and psi, compose with that, and curry

[Adam Topaz]

import Mathlib

universe u v w x

variable {R : Type u} [CommSemiring R]
variable {A : Type v} [AddCommMonoid A] [Module R A]
variable {B : Type w} [AddCommMonoid B] [Module R B]
variable (S : Type x) [Semiring S] [Algebra R S]

open scoped TensorProduct

def do_we_have_this (φ : A →ₗ[R] S) (ψ : B →ₗ[R] S) : A →ₗ[R] B →ₗ[R] S :=
  let a : A ⊗[R] B →ₗ[R] S ⊗[R] S := TensorProduct.map φ ψ
  let μ : S ⊗[R] S →ₗ[R] S := LinearMap.mul' R S
  let t := μ.comp a
  TensorProduct.curry t

example (φ : A →ₗ[R] S) (ψ : B →ₗ[R] S) (a : A) (b : B) :
  do_we_have_this S φ ψ a b  = φ a * ψ b := rfl

[Adam Topaz]

mostly all found with exact?

[Kevin Buzzard]

Nice. I'd been using exact? to go from do_we_have_this to the following question (which I don't have the answer to, and probably it would be easier to figure it out with pencil and paper): is there a contravariant monoid functor on (commutative) R-algebras attached to a CoAlgebra?

import Mathlib

suppress_compilation

universe u v w x

open TensorProduct

namespace Coalgebra
variable {R : Type u} {A : Type v}
variable [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A]
variable {S : Type w} [Semiring S] [Algebra R S] --Maybe commSemiring needed?

variable {B : Type x} [AddCommMonoid B] [Module R B] in
abbrev do_we_have_this (φ : A →ₗ[R] S) (ψ : B →ₗ[R] S) : A →ₗ[R] B →ₗ[R] S :=
  let a : A ⊗[R] B →ₗ[R] S ⊗[R] S := TensorProduct.map φ ψ
  let μ : S ⊗[R] S →ₗ[R] S := LinearMap.mul' R S
  let t := μ.comp a
  TensorProduct.curry t

/-- The `1` for the possible monoid structure on `A →ₗ[R] S` comes from the counit
of the coalgebra structure on `A` (composed with the canonical `R`-linear map `R →ₗ[R] S`). -/
def one : A →ₗ[R] S := (Algebra.linearMap R S).comp counit

/-- The `*` for the possible monoid structure on `A →ₗ[R] S` -/
def mul (φ ψ : A →ₗ[R] S) : (A →ₗ[R] S) :=
    (TensorProduct.lift (do_we_have_this φ ψ) : A ⊗[R] A →ₗ[R] S).comp comul

-- Is this a monoid?

lemma one_mul (φ : A →ₗ[R] S) : mul one φ = φ := by
  sorry

lemma mul_one (φ : A →ₗ[R] S) : mul φ one = φ := by
  sorry

lemma mul_assoc (φ ψ ρ : A →ₗ[R] S) : mul (mul φ ψ) ρ = mul φ (mul ψ ρ) := by
  sorry

These sorrys could well not be provable. I'm not particularly convinced that there is; if A is a Bialgebra then you probably get a monoid structure on the R-algebra morphisms to S (as you can guess I'm thinking about group functors), and I was wondering if this was a submonoid of a possible monoid structure on the bigger space of R-linear maps.

[Adam Topaz]

So an R algebra is “just” a monoid in the monoidal category of R-modules (with the usual tensor product). So yes, Hom(-,S) should take values in monoids

[Kevin Buzzard]

I'm a bit unclear about what you're claiming: which kind of homs do you mean by Hom(-,S)? Note that I'm doing coalgebras not algebras (and currently trying to understand them; I know nothing)

[Kevin Buzzard]

Oh I see from Wikipedia that (at least over fields R) Hom_{R-mod}(R-coalgebra,R) is an algebra? Is that what it's saying?

[Adam Topaz]

sorry, I don't know what I'm saying. I was getting my kids ready for ski lessons and was only half reading/thinking

[Adam Topaz]

what is definitely true is that a (co)algebra over $R$ is the same thing as a (co)monoid in the monoidal category of $R$-modules (in the sense of docs#Mon_ for instance)

[Eric Wieser]

I think this is (LinearMap.mul R S).compl₁₂? (docs#LinearMap.compl₁₂)

[Kevin Buzzard]

Wait what is a comonoid object in a monoidal category?

[Kevin Buzzard]

All I want is a connected reductive group over a field and they're all affine

[Kevin Buzzard]

I was wondering whether I should just use Hopf algebras to model these.

[Kevin Buzzard]

And then I went down a rabbit hole

[Kevin Buzzard]

What structure do you need on a category for it to admit coalgebras? Eg vector spaces over a fixed ground field (or commsemiring) seems to work. Is there such a thing as a cosemigroup?

[Kevin Buzzard]

@Reid Barton do you understand this twaddle?

[Kevin Buzzard]

So maybe there's the concept of a "coalgebra object" in any monoidal category, and probably modules over a semiring are a monoidal category?

[Kevin Buzzard]

As are R-algebras and commutative R-algebras?

[Kevin Buzzard]

aha maybe I've got it: is it something like: a coalgebra is a coalgebra object in the category of R-modules, a Hopf algebra is a coalgebra object in the category of (commutative?) R-algebras?

[Kevin Buzzard]

and a bialgebra is some weird in-between thing?

[Kim Morrison]

Kevin, Hopf algebras are a bit more complicated, so let's get the bialgebra story straight first. :-)

The usual way to describe a bialgebra is as something that is simultaneously an algebra and a coalgebra, and that the coalgebra structural morphisms are algebra maps and (in fact, equivalently) the algebra morphisms are coalgebra maps.

[Kim Morrison]

Another way to say that is that a bialgebra is a comonoid object in the category of monoid objects in the category of R-modules.

[Kim Morrison]

And inevitably that is equivalent to the monoid objects in the comonoid objects in R-mod.

[Adam Topaz]

Kevin Buzzard said:

All I want is a connected reductive group over a field and they're all affine

I think (affine) group schemes should be modeled as group objects in the category of (affine) schemes.

[Adam Topaz]

Do we have docs#Group_ ?

[Kim Morrison]

For the relation between Hopf algebras and group objects the summary at https://ncatlab.org/nlab/show/Hopf+algebra#relation_to_hopf_groups seems good.

[Kevin Buzzard]

Adam Topaz said:

Kevin Buzzard said:

All I want is a connected reductive group over a field and they're all affine

I think (affine) group schemes should be modeled as group objects in the category of (affine) schemes.

I want to implement them as commutative rings with extra structure because it's cheaper. I want to be able to do some trick like I did for elliptic curves, where I say "let K be a field and let 𝒞ℛ𝒢 denote the type of connected reductive groups over K and the user can have their $\mathbb{G}_m$ but secretly it's just `$R[X,X^{-1}]$.

[Kevin Buzzard]

Oh I'm a fool about bialgebras, I had got the definition wrong. Ignore most of my nonsense about monoid (co)objects above

[Kevin Buzzard]

Which side is simp normal form? (I see we use comul.lTensor in the definition of coalgebra.)

example : (comul.lTensor (R := R) A :
    A ⊗[R] A →ₗ[R] A ⊗[R] A ⊗[R] A) = TensorProduct.map LinearMap.id comul :=
  rfl

[Kevin Buzzard]

Do we have this?

import Mathlib

suppress_compilation

universe u w

open TensorProduct

variable {R : Type u} [CommSemiring R]
variable {S : Type w} [Semiring S] [Algebra R S]

-- dual of Coalgebra.coassoc
lemma Algebra.assoc : (LinearMap.mul' R S) ∘ₗ ((LinearMap.mul' R S).lTensor S) ∘ₗ (TensorProduct.assoc R S S S).toLinearMap
    = (LinearMap.mul' R S) ∘ₗ ((LinearMap.mul' R S).rTensor S) := by
  ext a b c
  simp
  -- `ring` doesn't work on mul_assoc.symm??
  convert (mul_assoc a b c).symm -- ??

[Kevin Buzzard]

I'm finally getting the hang of it. I'm annoyed that I have to use pen and paper sometimes and can't use Lean as a scratchpad.

import Mathlib

-- attribute [pp_dot] LinearMap.comp
-- attribute [pp_dot] LinearMap.mul'
-- attribute [pp_dot] LinearMap.id

suppress_compilation

universe u v w

open TensorProduct

namespace Coalgebra
variable {R : Type u} {A : Type v}
variable [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A]
variable {S : Type w} [Semiring S] [Algebra R S]

/-- A proposed `*` for a possible semigroup structure on `A →ₗ[R] S` -/
def mul (φ ψ : A →ₗ[R] S) : (A →ₗ[R] S) :=
(LinearMap.mul' R S).comp ((TensorProduct.map φ ψ).comp comul)

instance : Mul (A →ₗ[R] S) := ⟨mul⟩

/-- A -(comul)-> A ⊗ A -(φ ⊗ ψ)-> S ⊗ S -(* on S)-> S -/
lemma mul_def (φ ψ : A →ₗ[R] S) : φ * ψ =
(LinearMap.mul' R S).comp ((TensorProduct.map φ ψ).comp comul) := by rfl

variable (φ ψ ρ : A →ₗ[R] S)

-- dual of Coalgebra.coassoc
lemma Algebra.assoc :
    (LinearMap.mul' R S) ∘ₗ ((LinearMap.mul' R S).lTensor S) ∘ₗ (TensorProduct.assoc R S S S)
    = (LinearMap.mul' R S) ∘ₗ ((LinearMap.mul' R S).rTensor S) := by
  ext a b c
  simp
  -- `ring` doesn't work on mul_assoc.symm??
  -- something weird going on?
  exact (mul_assoc a b c).symm -- ??

lemma mul_assoc : (φ * ψ) * ρ = φ * (ψ * ρ) := by
  simp only [mul_def]
  -- worked out proof on paper
  -- first commutative square
  have h := (map_map_comp_assoc_eq φ ψ ρ).symm -- contains two `TensorProduct.assoc`s
  -- now glue on another one
  replace h := congr_arg (. ∘ₗ (LinearMap.rTensor A comul ∘ₗ comul : A →ₗ[R]  (A ⊗[R] A) ⊗[R] A)) h
  dsimp at h
  -- and another
  replace h := congr_arg (((LinearMap.mul' R S) ∘ₗ ((LinearMap.mul' R S).lTensor S)) ∘ₗ .) h
  dsimp at h
  -- now need to remove both `TensorProduct.assoc`s from h using associativity
  -- and coassociativity axioms
  have hSassoc := Algebra.assoc (R := R) (S := S)
  have hAassoc := coassoc (R := R) (A := A)
  -- comping one way
  simp only [← LinearMap.comp_assoc] at h hSassoc
  rw [hSassoc] at h
  -- comping the other way
  simp only [LinearMap.comp_assoc] at h hAassoc
  rw [hAassoc] at h
  simpa [← LinearMap.comp_assoc] using h

How am I supposed to be doing these calculations?

[Eric Wieser]

Kevin Buzzard said:

Which side is simp normal form? (I see we use comul.lTensor in the definition of coalgebra.)

example : (comul.lTensor (R := R) A :
    A ⊗[R] A →ₗ[R] A ⊗[R] A ⊗[R] A) = TensorProduct.map LinearMap.id comul :=
  rfl

In category theory land, there is a big refactor going on to try and make lTensor simp-normal

[Eric Wieser]

It might also be reasonable to make it reducible (outside of category theory) to make the question go away