Documentation

TauCeti.CategoryTheory.Monoidal.Cartesian.CommGrp

Commutative group objects form a preadditive category #

Let C be a braided cartesian monoidal category. For commutative group objects A and B of C, the morphisms A ⟶ B of CommGrp C form a commutative group under the pointwise group law of B: the sum of f and g is the composite lift f g ≫ μ, the product of f and g in the group A.X ⟶ B.X of points of B with values in A.X. Composition is additive on both sides, since precomposition preserves the group law on points and postcomposition with a homomorphism of group objects does too. Hence CommGrp C is a preadditive category, and the endomorphisms of a commutative group object form a ring (CategoryTheory.End.ring) whose multiplication is composition.

For commutative group schemes over a base scheme S, that is C = Over S, this is the abelian group of homomorphisms Hom_S(G, H) and the endomorphism ring End_S(G), in which an integer n acts as multiplication by n (CommGrp.intCast_hom_hom_hom).

The group law is written additively on morphisms of CommGrp C, while the group law on points of a group object is written multiplicatively (Mathlib's scoped instance CategoryTheory.Hom.group), so f + g corresponds to the product of the underlying morphisms (CommGrp.add_hom_hom_hom).

Main definitions #

Main results #

source
@[instance_reducible]
noncomputable instance CategoryTheory.CommGrp.instAddCommGroupHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A B : CommGrp C) :
AddCommGroup (A ⟶ B)

The commutative group of morphisms A ⟶ B of commutative group objects, under the pointwise group law of B, written additively. It is transported along InducedCategory.homEquiv from the commutative group of morphisms of group objects into the commutative group object B (Mathlib's Hom.commGroup in Grp C).

source
def CategoryTheory.CommGrp.homMk {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f : A.X ⟶ B.X) [IsMonHom f] :
A ⟶ B

Construct a morphism A ⟶ B of commutative group objects from a homomorphism of group objects f : A.X ⟶ B.X.

Instances For
    source
    @[simp]
    theorem CategoryTheory.CommGrp.homMk_hom_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f : A.X ⟶ B.X) [IsMonHom f] :
    (homMk f).hom.hom.hom = f

    The underlying morphism of homMk f is f.

    source
    @[simp]
    theorem CategoryTheory.CommGrp.add_hom_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f g : A ⟶ B) :
    (f + g).hom.hom.hom = f.hom.hom.hom * g.hom.hom.hom

    The sum of morphisms of commutative group objects is the product of the underlying morphisms for the group law on points.

    source
    @[simp]
    theorem CategoryTheory.CommGrp.zero_hom_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} :
    (InducedCategory.Hom.hom 0).hom.hom = 1

    The zero morphism of commutative group objects is the unit point toUnit _ ≫ η.

    source
    @[simp]
    theorem CategoryTheory.CommGrp.neg_hom_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f : A ⟶ B) :
    (-f).hom.hom.hom = f.hom.hom.hom⁻¹

    The negative of a morphism of commutative group objects is its inverse for the group law on points.

    source
    @[simp]
    theorem CategoryTheory.CommGrp.sub_hom_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f g : A ⟶ B) :
    (f - g).hom.hom.hom = f.hom.hom.hom / g.hom.hom.hom

    The difference of morphisms of commutative group objects is the quotient of the underlying morphisms for the group law on points.

    source
    @[simp]
    theorem CategoryTheory.CommGrp.nsmul_hom_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f : A ⟶ B) (n : ℕ) :
    (n • f).hom.hom.hom = f.hom.hom.hom ^ n

    A natural multiple of a morphism of commutative group objects is a power of the underlying morphism for the group law on points.

    source
    @[simp]
    theorem CategoryTheory.CommGrp.zsmul_hom_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f : A ⟶ B) (n : ℤ) :
    (n • f).hom.hom.hom = f.hom.hom.hom ^ n

    An integer multiple of a morphism of commutative group objects is a power of the underlying morphism for the group law on points.

    source
    @[instance_reducible]
    noncomputable instance CategoryTheory.CommGrp.instPreadditive {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
    Preadditive (CommGrp C)

    Commutative group objects form a preadditive category. Composition of morphisms of commutative group objects is additive in each variable.

    source
    @[simp]
    theorem CategoryTheory.CommGrp.intCast_hom_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) (n : ℤ) :
    (↑n).asHom.hom.hom.hom = CategoryStruct.id A.X ^ n

    The integer n in the endomorphism ring of a commutative group object A is multiplication by n: the n-th power of the identity of A.X for the group law on points.

    source
    @[simp]
    theorem CategoryTheory.CommGrp.natCast_hom_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) (n : ℕ) :
    (↑n).asHom.hom.hom.hom = CategoryStruct.id A.X ^ n

    The natural number n in the endomorphism ring of a commutative group object A is multiplication by n: the n-th power of the identity of A.X for the group law on points.

    source
    @[simp]
    theorem CategoryTheory.Functor.mapCommGrp_map_intCast {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) (n : ℤ) :
    F.mapCommGrp.map (↑n).asHom = (↑n).asHom

    A braided functor takes multiplication by an integer n on a commutative group object A to multiplication by n on the image of A.

    source
    @[simp]
    theorem CategoryTheory.Functor.mapCommGrp_map_natCast {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) (n : ℕ) :
    F.mapCommGrp.map (↑n).asHom = (↑n).asHom

    A braided functor takes multiplication by a natural number n on a commutative group object A to multiplication by n on the image of A.