Bilinear and alternating morphisms of monoid objects

Let C be a cartesian monoidal category and A, B, M monoid objects of C. For every object T, the morphisms T ⟶ A (the T-valued points of A) form a monoid under the pointwise product (Mathlib's CategoryTheory.Hom.monoid, scoped in CategoryTheory.MonObj). A morphism e : A ⊗ B ⟶ M is bilinear (TauCeti.CategoryTheory.IsBilinear) if, for every T, the pairing (a, b) ↦ lift a b ≫ e of T-valued points is multiplicative in each variable, and a morphism e : A ⊗ A ⟶ M is alternating (TauCeti.CategoryTheory.IsAlternating) if lift a a ≫ e = 1 for every point a. For group schemes over a base S, that is C = Over S, these are the bilinear and alternating pairings of group schemes, such as the Weil pairing E[N] ×_S E[N] ⟶ μ_N.

Both conditions are stated on points, so they are preserved by every monoidal functor between cartesian monoidal categories, which preserves points, products and the pointwise product. For a faithful functor they are also reflected, so the bijection between morphisms A ⊗ B ⟶ M and F.obj A ⊗ F.obj B ⟶ F.obj M given by a fully faithful monoidal functor (CategoryTheory.Functor.FullyFaithful.tensorHomEquiv, in TauCeti.CategoryTheory.Monoidal.Functor) matches bilinear and alternating morphisms on the two sides. Applied to an equivalence of categories, such as Grothendieck's Galois correspondence between finite étale schemes over a field and finite continuous Galois sets, this transports alternating pairings of group objects.

Main definitions

• TauCeti.CategoryTheory.IsBilinear e: the morphism e : A ⊗ B ⟶ M is bilinear.
• TauCeti.CategoryTheory.IsAlternating e: the morphism e : A ⊗ A ⟶ M vanishes on the diagonal.

Main results

• TauCeti.CategoryTheory.isAlternating_iff: alternation is the single identity lift (𝟙 A) (𝟙 A) ≫ e = 1 for the universal point.
• TauCeti.CategoryTheory.IsBilinear.map and TauCeti.CategoryTheory.IsAlternating.map: monoidal functors preserve bilinear and alternating morphisms.
• CategoryTheory.Functor.isBilinear_map_iff and CategoryTheory.Functor.isAlternating_map_iff: faithful monoidal functors reflect them.

structure TauCeti.CategoryTheory.IsBilinear {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B M : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] (e : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ M) : Prop

A morphism e : A ⊗ B ⟶ M of monoid objects is bilinear if the induced pairing (a, b) ↦ lift a b ≫ e on T-valued points is multiplicative in each variable, for every object T.

• lift_mul_left {T : C} (a a' : T ⟶ A) (b : T ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (a * a') b) e = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift a b) e * CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift a' b) e

  Multiplicativity in the first variable.

• lift_mul_right {T : C} (a : T ⟶ A) (b b' : T ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift a (b * b')) e = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift a b) e * CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift a b') e

  Multiplicativity in the second variable.

def TauCeti.CategoryTheory.IsAlternating {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A M : C} [CategoryTheory.MonObj M] (e : CategoryTheory.MonoidalCategoryStruct.tensorObj A A ⟶ M) : Prop

A morphism e : A ⊗ A ⟶ M into a monoid object is alternating if it is trivial on the diagonal: lift a a ≫ e = 1 for every T-valued point a of A.

theorem TauCeti.CategoryTheory.isAlternating_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A M : C} [CategoryTheory.MonObj M] {e : CategoryTheory.MonoidalCategoryStruct.tensorObj A A ⟶ M} : IsAlternating e ↔ ∀ ⦃T : C⦄ (a : T ⟶ A), CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift a a) e = 1

Unfolding IsAlternating: e is alternating if and only if lift a a ≫ e = 1 for every T-valued point a of A.

@[simp]

theorem TauCeti.CategoryTheory.IsAlternating.lift_self {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A M : C} [CategoryTheory.MonObj M] {e : CategoryTheory.MonoidalCategoryStruct.tensorObj A A ⟶ M} (h : IsAlternating e) {T : C} (a : T ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift a a) e = 1

An alternating morphism is trivial on every diagonal point lift a a.

theorem TauCeti.CategoryTheory.isAlternating_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A M : C} [CategoryTheory.MonObj M] {e : CategoryTheory.MonoidalCategoryStruct.tensorObj A A ⟶ M} : IsAlternating e ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A) (CategoryTheory.CategoryStruct.id A)) e = 1

Alternation is a single identity, for the universal point 𝟙 A: every point a : T ⟶ A factors as a ≫ 𝟙 A.

theorem TauCeti.CategoryTheory.IsBilinear.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B M : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] {N : C} [CategoryTheory.MonObj N] {e : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ M} (h : IsBilinear e) (g : M ⟶ N) [CategoryTheory.IsMonHom g] : IsBilinear (CategoryTheory.CategoryStruct.comp e g)

Postcomposing a bilinear morphism with a homomorphism of monoid objects gives a bilinear morphism.

theorem TauCeti.CategoryTheory.IsBilinear.tensorHom_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B M : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] {A' B' : C} [CategoryTheory.MonObj A'] [CategoryTheory.MonObj B'] {e : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ M} (h : IsBilinear e) (f : A' ⟶ A) (g : B' ⟶ B) [CategoryTheory.IsMonHom f] [CategoryTheory.IsMonHom g] : IsBilinear (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) e)

Precomposing a bilinear morphism with homomorphisms of monoid objects in each variable gives a bilinear morphism.

theorem TauCeti.CategoryTheory.IsAlternating.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A M : C} [CategoryTheory.MonObj M] {N : C} [CategoryTheory.MonObj N] {e : CategoryTheory.MonoidalCategoryStruct.tensorObj A A ⟶ M} (h : IsAlternating e) (g : M ⟶ N) [CategoryTheory.IsMonHom g] : IsAlternating (CategoryTheory.CategoryStruct.comp e g)

Postcomposing an alternating morphism with a homomorphism of monoid objects gives an alternating morphism.

theorem TauCeti.CategoryTheory.IsAlternating.tensorHom_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A M : C} [CategoryTheory.MonObj M] {A' : C} {e : CategoryTheory.MonoidalCategoryStruct.tensorObj A A ⟶ M} (h : IsAlternating e) (f : A' ⟶ A) : IsAlternating (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) e)

Precomposing an alternating morphism with f ⊗ₘ f gives an alternating morphism.

theorem TauCeti.CategoryTheory.IsBilinear.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Monoidal] {A B M : C} [CategoryTheory.MonObj M] [CategoryTheory.MonObj A] [CategoryTheory.MonObj B] {e : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ M} (h : IsBilinear e) : IsBilinear (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A B) (F.map e))

A monoidal functor between cartesian monoidal categories preserves bilinear morphisms: if e : A ⊗ B ⟶ M is bilinear, so is μ F A B ≫ F.map e : F.obj A ⊗ F.obj B ⟶ F.obj M.

theorem TauCeti.CategoryTheory.IsAlternating.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.CartesianMonoidalCategory D] (F : CategoryTheory.Functor C D) [F.Monoidal] {A M : C} [CategoryTheory.MonObj M] {e : CategoryTheory.MonoidalCategoryStruct.tensorObj A A ⟶ M} (h : IsAlternating e) : IsAlternating (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A A) (F.map e))

A monoidal functor between cartesian monoidal categories preserves alternating morphisms: if e : A ⊗ A ⟶ M is alternating, so is μ F A A ≫ F.map e.

theorem CategoryTheory.Functor.isBilinear_map_iff {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} [F.Monoidal] {A B M : C} [MonObj M] [F.Faithful] [MonObj A] [MonObj B] {e : MonoidalCategoryStruct.tensorObj A B ⟶ M} : TauCeti.CategoryTheory.IsBilinear (CategoryStruct.comp (LaxMonoidal.μ F A B) (F.map e)) ↔ TauCeti.CategoryTheory.IsBilinear e

A faithful monoidal functor between cartesian monoidal categories reflects bilinear morphisms.

theorem CategoryTheory.Functor.isAlternating_map_iff {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} [F.Monoidal] {A M : C} [MonObj M] [F.Faithful] {e : MonoidalCategoryStruct.tensorObj A A ⟶ M} : TauCeti.CategoryTheory.IsAlternating (CategoryStruct.comp (LaxMonoidal.μ F A A) (F.map e)) ↔ TauCeti.CategoryTheory.IsAlternating e

A faithful monoidal functor between cartesian monoidal categories reflects alternating morphisms.