Objectwise congruence invariance of categorical group actions

For a group H acting on C and a family of subgroups K : ℕ → Subgroup H, congruenceInvariant K is the object property that some K N, with 0 < N, fixes the object up to isomorphism. IsObjectwiseCongruenceInvariant K C requires this for every object, allowing the bound to depend on the object.

Equivariant functors preserve this property, and fully faithful equivariant functors reflect it. Consequently it is invariant under equivariant equivalence and restricts to invariant full subcategories. Equivariance uses Mathlib's Functor.LeftLinear; restriction uses the native full-subcategory action.

The fixing isomorphisms are only required to exist separately for each group element. They carry no multiplication coherence or rational integration data. No normality or monotonicity of K is needed for these comparisons.

References

congruenceInvariant follows the objectwise K_N-invariance condition in Frenkel's local-category discussion:

• Edward Frenkel, Langlands Correspondence for Loop Groups, §1.3.4 (congruence subgroups and stability under twisting).
• Edward Frenkel and Dennis Gaitsgory, Local geometric Langlands correspondence and affine Kac–Moody algebras.

def TauCeti.congruenceInvariant {H : Type u_1} [Group H] (K : ℕ → Subgroup H) {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] : CategoryTheory.ObjectProperty C

Objects fixed up to isomorphism by some positive-indexed congruence subgroup. The isomorphisms need not satisfy any coherence condition.

theorem TauCeti.congruenceInvariant_iff {H : Type u_1} [Group H] (K : ℕ → Subgroup H) {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] (X : C) : congruenceInvariant K X ↔ ∃ (N : ℕ), 0 < N ∧ ∀ g ∈ K N, Nonempty (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj { as := g } X ≅ X)

def TauCeti.IsObjectwiseCongruenceInvariant {H : Type u_1} [Group H] (K : ℕ → Subgroup H) (C : Type u_3) [CategoryTheory.Category.{v_2, u_3} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] : Prop

Every object is fixed up to isomorphism by a positive-indexed congruence subgroup; the subgroup may depend on the object.

theorem TauCeti.isObjectwiseCongruenceInvariant_iff {H : Type u_1} [Group H] (K : ℕ → Subgroup H) {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] : IsObjectwiseCongruenceInvariant K C ↔ ∀ (X : C), congruenceInvariant K X

instance TauCeti.instIsClosedUnderIsomorphismsCongruenceInvariant {H : Type u_1} [Group H] (K : ℕ → Subgroup H) {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] : (congruenceInvariant K).IsClosedUnderIsomorphisms

theorem TauCeti.congruenceInvariant_map {H : Type u_1} [Group H] {K : ℕ → Subgroup H} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] {D : Type u_3} [CategoryTheory.Category.{v_2, u_3} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) D] (F : CategoryTheory.Functor C D) [F.LeftLinear (CategoryTheory.Discrete H)] {X : C} (hX : congruenceInvariant K X) : congruenceInvariant K (F.obj X)

An equivariant functor preserves the fixing subgroup of each object.

theorem TauCeti.congruenceInvariant_of_map {H : Type u_1} [Group H] {K : ℕ → Subgroup H} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] {D : Type u_3} [CategoryTheory.Category.{v_2, u_3} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) D] (F : CategoryTheory.Functor C D) [F.LeftLinear (CategoryTheory.Discrete H)] [F.Full] [F.Faithful] {X : C} (hX : congruenceInvariant K (F.obj X)) : congruenceInvariant K X

A fully faithful equivariant functor reflects the fixing subgroup of each object.

@[simp]

theorem TauCeti.congruenceInvariant_map_iff {H : Type u_1} [Group H] {K : ℕ → Subgroup H} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] {D : Type u_3} [CategoryTheory.Category.{v_2, u_3} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) D] (F : CategoryTheory.Functor C D) [F.LeftLinear (CategoryTheory.Discrete H)] [F.Full] [F.Faithful] (X : C) : congruenceInvariant K (F.obj X) ↔ congruenceInvariant K X

theorem TauCeti.IsObjectwiseCongruenceInvariant.of_essSurj {H : Type u_1} [Group H] {K : ℕ → Subgroup H} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] {D : Type u_3} [CategoryTheory.Category.{v_2, u_3} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) D] (h : IsObjectwiseCongruenceInvariant K C) (F : CategoryTheory.Functor C D) [F.LeftLinear (CategoryTheory.Discrete H)] [F.EssSurj] : IsObjectwiseCongruenceInvariant K D

Essential surjectivity lets an equivariant functor transfer objectwise congruence invariance to its entire target category.

theorem TauCeti.IsObjectwiseCongruenceInvariant.of_fullyFaithful {H : Type u_1} [Group H] {K : ℕ → Subgroup H} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] {D : Type u_3} [CategoryTheory.Category.{v_2, u_3} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) D] (h : IsObjectwiseCongruenceInvariant K D) (F : CategoryTheory.Functor C D) [F.LeftLinear (CategoryTheory.Discrete H)] [F.Full] [F.Faithful] : IsObjectwiseCongruenceInvariant K C

Objectwise congruence invariance pulls back along a fully faithful equivariant functor.

theorem TauCeti.isObjectwiseCongruenceInvariant_iff_of_equivalence {H : Type u_1} [Group H] {K : ℕ → Subgroup H} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] {D : Type u_3} [CategoryTheory.Category.{v_2, u_3} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) D] (e : C ≌ D) [e.functor.LeftLinear (CategoryTheory.Discrete H)] : IsObjectwiseCongruenceInvariant K C ↔ IsObjectwiseCongruenceInvariant K D

Objectwise congruence invariance is independent of an equivariant presentation of the category. Only the forward functor of the equivalence needs a specified lineator.

@[simp]

theorem TauCeti.congruenceInvariant_fullSubcategory_iff {H : Type u_1} [Group H] (K : ℕ → Subgroup H) {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.IsStableUnderLeftAction (CategoryTheory.Discrete H) P] (X : P.FullSubcategory) : congruenceInvariant K X ↔ congruenceInvariant K X.obj

For a stable full subcategory, congruence invariance of an object is equivalent to congruence invariance of its underlying ambient object, with the same fixing subgroup.

@[simp]

theorem TauCeti.isObjectwiseCongruenceInvariant_fullSubcategory_iff {H : Type u_1} [Group H] (K : ℕ → Subgroup H) {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.IsStableUnderLeftAction (CategoryTheory.Discrete H) P] : IsObjectwiseCongruenceInvariant K P.FullSubcategory ↔ P ≤ congruenceInvariant K

A stable full subcategory is objectwise congruence invariant exactly when all objects satisfying its defining property are congruence invariant in the ambient category.

theorem TauCeti.IsObjectwiseCongruenceInvariant.fullSubcategory {H : Type u_1} [Group H] (K : ℕ → Subgroup H) {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.IsStableUnderLeftAction (CategoryTheory.Discrete H) P] (h : IsObjectwiseCongruenceInvariant K C) : IsObjectwiseCongruenceInvariant K P.FullSubcategory

Restricting an objectwise congruence invariant action to a stable full subcategory preserves objectwise congruence invariance.