Documentation

TauCeti.CategoryTheory.FiniteBijection

The finite-bijection groupoid #

The groupoid FiniteBijection has one object mk n for each natural number n, and its morphisms mk n ⟶ mk m are the bijections Fin n ≃ Fin m. It is the standard skeleton of the groupoid of finite sets and bijections, and its automorphism group at mk n is the symmetric group Equiv.Perm (Fin n).

Block sum makes it a symmetric monoidal category: the tensor product of mk n and mk m is mk (n + m), a pair of bijections acts on the two blocks Fin.castAdd and Fin.natAdd separately, and the braiding is the block swap finAddFlip. The associator and unitors are the casts along Nat.add_assoc, Nat.zero_add and Nat.add_zero.

Functors out of this symmetric monoidal groupoid are symmetric sequences, and Day convolution along its block sum is the product of symmetric sequences used to define symmetric spectra.

References #

M. Hovey, B. Shipley and J. Smith, Symmetric spectra, J. Amer. Math. Soc. 13 (2000), Section 2.1.

structure TauCeti.FiniteBijection :

The finite-bijection groupoid: an object is a natural number n, standing for the standard finite set Fin n.

len : ℕ
The cardinality of the standard finite set an object stands for.

Instances For

theorem TauCeti.FiniteBijection.ext_iff {x y : FiniteBijection} :

x = y ↔ x.len = y.len

theorem TauCeti.FiniteBijection.ext {x y : FiniteBijection} (len : x.len = y.len) :

x = y

@[simp]

theorem TauCeti.FiniteBijection.mk_len (n : FiniteBijection) :

{ len := n.len } = n

structure TauCeti.FiniteBijection.Hom (n m : FiniteBijection) :

A morphism of FiniteBijection is a bijection of the standard finite sets.

toEquiv : Fin n.len ≃ Fin m.len
The bijection underlying a morphism.

Instances For

theorem TauCeti.FiniteBijection.Hom.ext_iff {n m : FiniteBijection} {x y : n.Hom m} :

x = y ↔ x.toEquiv = y.toEquiv

theorem TauCeti.FiniteBijection.Hom.ext {n m : FiniteBijection} {x y : n.Hom m} (toEquiv : x.toEquiv = y.toEquiv) :

x = y

@[instance_reducible]

instance TauCeti.FiniteBijection.instGroupoid :

CategoryTheory.Groupoid FiniteBijection

theorem TauCeti.FiniteBijection.hom_ext {n m : FiniteBijection} {f g : n ⟶ m} (h : ∀ (i : Fin n.len), f.toEquiv i = g.toEquiv i) :

f = g

theorem TauCeti.FiniteBijection.hom_ext_iff {n m : FiniteBijection} {f g : n ⟶ m} :

f = g ↔ ∀ (i : Fin n.len), f.toEquiv i = g.toEquiv i

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_id (n : FiniteBijection) :

(CategoryTheory.CategoryStruct.id n).toEquiv = Equiv.refl (Fin n.len)

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_comp {n m k : FiniteBijection} (f : n ⟶ m) (g : m ⟶ k) :

(CategoryTheory.CategoryStruct.comp f g).toEquiv = f.toEquiv.trans g.toEquiv

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_inv {n m : FiniteBijection} (f : n ⟶ m) :

(CategoryTheory.inv f).toEquiv = f.toEquiv.symm

def TauCeti.FiniteBijection.isoMk {n m : FiniteBijection} (e : Fin n.len ≃ Fin m.len) :

n ≅ m

The isomorphism of FiniteBijection given by a bijection of the standard finite sets.

Instances For

@[simp]

theorem TauCeti.FiniteBijection.isoMk_inv_toEquiv {n m : FiniteBijection} (e : Fin n.len ≃ Fin m.len) :

(isoMk e).inv.toEquiv = e.symm

@[simp]

theorem TauCeti.FiniteBijection.isoMk_hom_toEquiv {n m : FiniteBijection} (e : Fin n.len ≃ Fin m.len) :

(isoMk e).hom.toEquiv = e

def TauCeti.FiniteBijection.isoEquiv {n m : FiniteBijection} :

(n ≅ m) ≃ (Fin n.len ≃ Fin m.len)

Isomorphisms of FiniteBijection are the bijections of the standard finite sets.

Instances For

@[simp]

theorem TauCeti.FiniteBijection.isoEquiv_symm_apply {n m : FiniteBijection} (e : Fin n.len ≃ Fin m.len) :

isoEquiv.symm e = isoMk e

@[simp]

theorem TauCeti.FiniteBijection.isoEquiv_apply {n m : FiniteBijection} (e : n ≅ m) :

isoEquiv e = e.hom.toEquiv

theorem TauCeti.FiniteBijection.skeletal :

CategoryTheory.Skeletal FiniteBijection

Two objects of FiniteBijection are isomorphic only if they are equal.

theorem TauCeti.FiniteBijection.eq_of_hom {n m : FiniteBijection} (f : n ⟶ m) :

n = m

FiniteBijection has morphisms only between equal objects.

def TauCeti.FiniteBijection.autMulEquiv (n : FiniteBijection) :

CategoryTheory.Aut n ≃* Equiv.Perm (Fin n.len)

The automorphism group of an object of FiniteBijection is the symmetric group of the standard finite set it stands for.

Instances For

@[simp]

theorem TauCeti.FiniteBijection.autMulEquiv_apply (n : FiniteBijection) (e : CategoryTheory.Aut n) :

n.autMulEquiv e = e.asIso.hom.toEquiv

@[simp]

theorem TauCeti.FiniteBijection.autMulEquiv_symm_apply_asIso (n : FiniteBijection) (σ : Equiv.Perm (Fin n.len)) :

(n.autMulEquiv.symm σ).asIso = isoMk σ

The block-sum symmetric monoidal structure #

@[instance_reducible]

instance TauCeti.FiniteBijection.instMonoidalCategoryStruct :

CategoryTheory.MonoidalCategoryStruct FiniteBijection

theorem TauCeti.FiniteBijection.tensorObj_len (n m : FiniteBijection) :

(CategoryTheory.MonoidalCategoryStruct.tensorObj n m).len = n.len + m.len

theorem TauCeti.FiniteBijection.tensorUnit_len :

(CategoryTheory.MonoidalCategoryStruct.tensorUnit FiniteBijection).len = 0

instance TauCeti.FiniteBijection.instSubsingletonHomTensorUnit (n : FiniteBijection) :

Subsingleton (CategoryTheory.MonoidalCategoryStruct.tensorUnit FiniteBijection ⟶ n)

There is at most one morphism out of the tensor unit mk 0, the empty bijection. In particular the only endomorphism of the tensor unit is the identity.

instance TauCeti.FiniteBijection.instIsEmptyHomTensorUnitMkHAddNatOfNat (n : ℕ) :

IsEmpty (CategoryTheory.MonoidalCategoryStruct.tensorUnit FiniteBijection ⟶ { len := n + 1 })

There is no morphism from the tensor unit mk 0 to a nonempty standard finite set.

theorem TauCeti.FiniteBijection.toEquiv_tensorHom {n m n' m' : FiniteBijection} (f : n ⟶ m) (g : n' ⟶ m') :

(CategoryTheory.MonoidalCategoryStruct.tensorHom f g).toEquiv = finSumFinEquiv.symm.trans ((f.toEquiv.sumCongr g.toEquiv).trans finSumFinEquiv)

theorem TauCeti.FiniteBijection.toEquiv_whiskerLeft (n : FiniteBijection) {m m' : FiniteBijection} (g : m ⟶ m') :

(CategoryTheory.MonoidalCategoryStruct.whiskerLeft n g).toEquiv = finSumFinEquiv.symm.trans (((Equiv.refl (Fin n.len)).sumCongr g.toEquiv).trans finSumFinEquiv)

theorem TauCeti.FiniteBijection.toEquiv_whiskerRight {n n' : FiniteBijection} (f : n ⟶ n') (m : FiniteBijection) :

(CategoryTheory.MonoidalCategoryStruct.whiskerRight f m).toEquiv = finSumFinEquiv.symm.trans ((f.toEquiv.sumCongr (Equiv.refl (Fin m.len))).trans finSumFinEquiv)

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_tensorHom_castAdd {n m n' m' : FiniteBijection} (f : n ⟶ m) (g : n' ⟶ m') (i : Fin n.len) :

(CategoryTheory.MonoidalCategoryStruct.tensorHom f g).toEquiv (Fin.castAdd n'.len i) = Fin.castAdd m'.len (f.toEquiv i)

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_tensorHom_natAdd {n m n' m' : FiniteBijection} (f : n ⟶ m) (g : n' ⟶ m') (i : Fin n'.len) :

(CategoryTheory.MonoidalCategoryStruct.tensorHom f g).toEquiv (Fin.natAdd n.len i) = Fin.natAdd m.len (g.toEquiv i)

@[simp]

theorem TauCeti.FiniteBijection.tensorHom_inj {n m n' m' : FiniteBijection} {f f' : n ⟶ m} {g g' : n' ⟶ m'} :

CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.MonoidalCategoryStruct.tensorHom f' g' ↔ f = f' ∧ g = g'

A tensor product of bijections determines its two factors.

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_whiskerLeft_castAdd (n : FiniteBijection) {m m' : FiniteBijection} (g : m ⟶ m') (i : Fin n.len) :

(CategoryTheory.MonoidalCategoryStruct.whiskerLeft n g).toEquiv (Fin.castAdd m.len i) = Fin.castAdd m'.len i

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_whiskerLeft_natAdd (n : FiniteBijection) {m m' : FiniteBijection} (g : m ⟶ m') (i : Fin m.len) :

(CategoryTheory.MonoidalCategoryStruct.whiskerLeft n g).toEquiv (Fin.natAdd n.len i) = Fin.natAdd n.len (g.toEquiv i)

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_whiskerRight_castAdd {n n' : FiniteBijection} (f : n ⟶ n') (m : FiniteBijection) (i : Fin n.len) :

(CategoryTheory.MonoidalCategoryStruct.whiskerRight f m).toEquiv (Fin.castAdd m.len i) = Fin.castAdd m.len (f.toEquiv i)

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_whiskerRight_natAdd {n n' : FiniteBijection} (f : n ⟶ n') (m : FiniteBijection) (i : Fin m.len) :

(CategoryTheory.MonoidalCategoryStruct.whiskerRight f m).toEquiv (Fin.natAdd n.len i) = Fin.natAdd n'.len i

theorem TauCeti.FiniteBijection.toEquiv_associator_hom (n m k : FiniteBijection) :

(CategoryTheory.MonoidalCategoryStruct.associator n m k).hom.toEquiv = finCongr ⋯

theorem TauCeti.FiniteBijection.toEquiv_associator_inv (n m k : FiniteBijection) :

(CategoryTheory.MonoidalCategoryStruct.associator n m k).inv.toEquiv = finCongr ⋯

theorem TauCeti.FiniteBijection.toEquiv_leftUnitor_hom (n : FiniteBijection) :

(CategoryTheory.MonoidalCategoryStruct.leftUnitor n).hom.toEquiv = finCongr ⋯

theorem TauCeti.FiniteBijection.toEquiv_leftUnitor_inv (n : FiniteBijection) :

(CategoryTheory.MonoidalCategoryStruct.leftUnitor n).inv.toEquiv = finCongr ⋯

theorem TauCeti.FiniteBijection.toEquiv_rightUnitor_hom (n : FiniteBijection) :

(CategoryTheory.MonoidalCategoryStruct.rightUnitor n).hom.toEquiv = finCongr ⋯

theorem TauCeti.FiniteBijection.toEquiv_rightUnitor_inv (n : FiniteBijection) :

(CategoryTheory.MonoidalCategoryStruct.rightUnitor n).inv.toEquiv = finCongr ⋯

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_associator_hom_castAdd_castAdd (n m k : FiniteBijection) (i : Fin n.len) :

(CategoryTheory.MonoidalCategoryStruct.associator n m k).hom.toEquiv (Fin.castAdd k.len (Fin.castAdd m.len i)) = Fin.castAdd (CategoryTheory.MonoidalCategoryStruct.tensorObj m k).len i

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_associator_hom_castAdd_natAdd (n m k : FiniteBijection) (i : Fin m.len) :

(CategoryTheory.MonoidalCategoryStruct.associator n m k).hom.toEquiv (Fin.castAdd k.len (Fin.natAdd n.len i)) = Fin.natAdd n.len (Fin.castAdd k.len i)

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_associator_hom_natAdd (n m k : FiniteBijection) (i : Fin k.len) :

(CategoryTheory.MonoidalCategoryStruct.associator n m k).hom.toEquiv (Fin.natAdd (CategoryTheory.MonoidalCategoryStruct.tensorObj n m).len i) = Fin.natAdd n.len (Fin.natAdd m.len i)

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_associator_inv_castAdd (n m k : FiniteBijection) (i : Fin n.len) :

(CategoryTheory.MonoidalCategoryStruct.associator n m k).inv.toEquiv (Fin.castAdd (CategoryTheory.MonoidalCategoryStruct.tensorObj m k).len i) = Fin.castAdd k.len (Fin.castAdd m.len i)

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_associator_inv_natAdd_castAdd (n m k : FiniteBijection) (i : Fin m.len) :

(CategoryTheory.MonoidalCategoryStruct.associator n m k).inv.toEquiv (Fin.natAdd n.len (Fin.castAdd k.len i)) = Fin.castAdd k.len (Fin.natAdd n.len i)

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_associator_inv_natAdd_natAdd (n m k : FiniteBijection) (i : Fin k.len) :

(CategoryTheory.MonoidalCategoryStruct.associator n m k).inv.toEquiv (Fin.natAdd n.len (Fin.natAdd m.len i)) = Fin.natAdd (CategoryTheory.MonoidalCategoryStruct.tensorObj n m).len i

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_leftUnitor_hom_natAdd (n : FiniteBijection) (i : Fin n.len) :

(CategoryTheory.MonoidalCategoryStruct.leftUnitor n).hom.toEquiv (Fin.natAdd (CategoryTheory.MonoidalCategoryStruct.tensorUnit FiniteBijection).len i) = i

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_leftUnitor_inv_apply (n : FiniteBijection) (i : Fin n.len) :

(CategoryTheory.MonoidalCategoryStruct.leftUnitor n).inv.toEquiv i = Fin.natAdd (CategoryTheory.MonoidalCategoryStruct.tensorUnit FiniteBijection).len i

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_rightUnitor_hom_castAdd (n : FiniteBijection) (i : Fin n.len) :

(CategoryTheory.MonoidalCategoryStruct.rightUnitor n).hom.toEquiv (Fin.castAdd (CategoryTheory.MonoidalCategoryStruct.tensorUnit FiniteBijection).len i) = i

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_rightUnitor_inv_apply (n : FiniteBijection) (i : Fin n.len) :

(CategoryTheory.MonoidalCategoryStruct.rightUnitor n).inv.toEquiv i = Fin.castAdd (CategoryTheory.MonoidalCategoryStruct.tensorUnit FiniteBijection).len i

@[instance_reducible]

instance TauCeti.FiniteBijection.instMonoidalCategory :

CategoryTheory.MonoidalCategory FiniteBijection

def TauCeti.FiniteBijection.braiding (n m : FiniteBijection) :

CategoryTheory.MonoidalCategoryStruct.tensorObj n m ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj m n

The block swap finAddFlip, as an isomorphism n ⊗ m ≅ m ⊗ n. This is the braiding β_ n m of the symmetric monoidal structure on FiniteBijection.

Instances For

@[instance_reducible]

instance TauCeti.FiniteBijection.instSymmetricCategory :

CategoryTheory.SymmetricCategory FiniteBijection

theorem TauCeti.FiniteBijection.toEquiv_braiding_hom (n m : FiniteBijection) :

(β_ n m).hom.toEquiv = finAddFlip

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_braiding_hom_castAdd (n m : FiniteBijection) (i : Fin n.len) :

(β_ n m).hom.toEquiv (Fin.castAdd m.len i) = Fin.natAdd m.len i

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_braiding_hom_natAdd (n m : FiniteBijection) (i : Fin m.len) :

(β_ n m).hom.toEquiv (Fin.natAdd n.len i) = Fin.castAdd n.len i

theorem TauCeti.FiniteBijection.toEquiv_braiding_inv (n m : FiniteBijection) :

(β_ n m).inv.toEquiv = finAddFlip

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_braiding_inv_castAdd (n m : FiniteBijection) (i : Fin m.len) :

(β_ n m).inv.toEquiv (Fin.castAdd n.len i) = Fin.natAdd n.len i

@[simp]

theorem TauCeti.FiniteBijection.toEquiv_braiding_inv_natAdd (n m : FiniteBijection) (i : Fin n.len) :

(β_ n m).inv.toEquiv (Fin.natAdd m.len i) = Fin.castAdd m.len i