ℂ-linearity of the embedding C ⥤ Ind C

For an arbitrary pair of ℂ-linear structures on C and on Ind C the embedding RS.indOf need not be ℂ-linear: two ring maps ℂ → End (𝟙_ (Ind C)) can differ by a field automorphism of ℂ, and nothing ties the structure upstairs to the one downstairs. That is why RS.IndOfLinear is carried as a hypothesis in RS.Classical.Deligne.GammaCountable.

The structures this development actually installs are not arbitrary. Both come from a single scalar unit ψ : ℂ ≃+* End (𝟙_ C), by RS.linearOfScalarUnit ψ downstairs and RS.linearOfScalarUnit (indScalarUnit ψ) upstairs, and RS.indScalarUnit ψ is by construction the transport of ψ along the embedding and the unit comparison RS.indOfUnitIso (RS.indScalarUnit_apply, which is a rfl). For that pair the scalar action on either side is conjugation of a unit endomorphism through the left unitor, and the embedding is strong monoidal (RS.indOfMonoidal), so it carries the one conjugate to the other: this is RS.indOf_map_scalarSmul.

This file reads that transport in the language of the installed module structures:

• RS.indOf_linear — indOf.map (c • f) = c • indOf.map f under the two letI-installed structures;
• RS.indOfFunctorLinear — the same, packaged as Mathlib's CategoryTheory.Functor.Linear ℂ indOf;
• RS.indOfLinear_of_scalarUnit — the same, in the shape RS.IndOfLinear C in which RS.Classical.Deligne.GammaCountable consumes it, so that the hypothesis is discharged for the scalar-unit structures.

The additive law is RS.indOf_additive; this module proves scalar compatibility. No compatibility between ψ and an ambient linear structure is asked, and no braiding is needed: both actions are defined from the same ψ, and the proof uses only the unitality of the strong monoidal structure of the embedding.

The scalar half, for the installed structures

theorem RS.indOf_linear {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) {X Y : C} (c : ℂ) (f : X ⟶ Y) : indOf.map (c • f) = c • indOf.map f

The embedding C ⥤ Ind C is ℂ-linear for the two ℂ-linear structures induced by a single scalar unit ψ: RS.scalarSmul is what • means on both sides, and RS.indOf_map_scalarSmul transports the one to the other.

theorem RS.indOfFunctorLinear {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) : CategoryTheory.Functor.Linear ℂ indOf

RS.indOf_linear, packaged as Mathlib's linearity class for a functor.

Discharging the hypothesis of the countability lane

theorem RS.indOfLinear_of_scalarUnit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) : IndOfLinear C

The ℂ-linearity hypothesis of RS.Classical.Deligne.GammaCountable holds for the scalar-unit structures: RS.IndOfLinear C is exactly RS.indOf_linear, read at the two structures induced by ψ.

Acceptance