Module

EquivariantIdempotentDescent.lean

Nyll.EtaleFundamentalGroups.Inertia.EquivariantIdempotentDescent

3 declarations indexed from sourceView source ↗

Module documentation

Finite equivariant idempotent families at one actual filtered stage

First descend the complete orthogonal family by the existing finite-product algebra construction. All of its group-equivariance equations then descend in one further transition, using a polynomial algebra with finitely many variables. The tensor factor carrying the action remains arbitrary.

The permutation representation of the finite index is explicit. The action on every tensor ring is the prescribed baseChangeAction, and the output retains each literal cocone image. This supplies the finite action data for the actual étale-neighborhood step of Stacks tag 0BST.

Imports7

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.AlgEquivDescent
Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.CoconeLeg
Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.IdempotentDescent
Nyll.EtaleFundamentalGroups.Inertia.InvariantBaseChange
Mathlib.Algebra.Category.Ring.Under.Basic
Mathlib.RingTheory.Idempotents
Mathlib.RingTheory.TensorProduct.Maps

Imported by3

instance

coefficientTensorAction

L42 ↗

EtaleFundamentalGroups.Inertia.coefficientTensorAction

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.Inertia
universe u w
variable {R : CommRingCat.{u}} {B : Type u} [CommRing B] [Algebra R B]
  {G : Type w} [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G R B]

Lean source · statement

instance coefficientTensorAction (A : Under R) : MulSemiringAction G (A ⊗[R] B)

theorem

exists_equivariant_refinement

L45 ↗

EtaleFundamentalGroups.Inertia.exists_equivariant_refinement

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.Inertia
universe u w
variable {R : CommRingCat.{u}} {B : Type u} [CommRing B] [Algebra R B]
  {G : Type w} [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G R B]
local instance coefficientTensorAction (A : Under R) : MulSemiringAction G (A ⊗[R] B) :=
  baseChangeAction R A B G

Lean source · statement

theorem exists_equivariant_refinement
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c) (k : J)
    {ι : Type u} [Fintype ι] (σ : G →* Equiv.Perm ι)
    (e : ι → (F.obj k ⊗[R] B)) (he : CompleteOrthogonalIdempotents e)
    (hσ : ∀ (g : G) (a : ι),
      filteredTensorToColimitAlgHom c k (g • e a) =
        filteredTensorToColimitAlgHom c k (e (σ g a))) :
    ∃ (l : J) (eₗ : ι → (F.obj l ⊗[R] B)),
      CompleteOrthogonalIdempotents eₗ ∧
        (∀ (g : G) (a : ι), g • eₗ a = eₗ (σ g a)) ∧
        ∀ a, filteredTensorToColimitAlgHom c l (eₗ a) =
          filteredTensorToColimitAlgHom c k (e a)

theorem

exists_equivariant_completeOrthogonalIdempotents_stage_of_filteredColimit

L79 ↗

EtaleFundamentalGroups.Inertia.exists_equivariant_completeOrthogonalIdempotents_stage_of_filteredColimit

Documentation

A finite complete equivariant family after tensor passage to a filtered colimit descends to one stage with all orthogonality, completeness, group equations, and literal cocone images preserved. No finite presentation of the acted-on algebra over the base is assumed.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups.Inertia
universe u w
variable {R : CommRingCat.{u}} {B : Type u} [CommRing B] [Algebra R B]
  {G : Type w} [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G R B]
local instance coefficientTensorAction (A : Under R) : MulSemiringAction G (A ⊗[R] B) :=
  baseChangeAction R A B G

Lean source · statement

theorem exists_equivariant_completeOrthogonalIdempotents_stage_of_filteredColimit
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    {ι : Type u} [Fintype ι] (σ : G →* Equiv.Perm ι)
    (e : ι → (c.pt ⊗[R] B)) (he : CompleteOrthogonalIdempotents e)
    (hσ : ∀ (g : G) (a : ι), g • e a = e (σ g a)) :
    ∃ (k : J) (eₖ : ι → (F.obj k ⊗[R] B)),
      CompleteOrthogonalIdempotents eₖ ∧
        (∀ (g : G) (a : ι), g • eₖ a = eₖ (σ g a)) ∧
        ∀ a, filteredTensorToColimitAlgHom c k (eₖ a) = e a

Module documentation

Finite equivariant idempotent families at one actual filtered stage

Declarations

coefficientTensorAction

exists_equivariant_refinement

exists_equivariant_completeOrthogonalIdempotents_stage_of_filteredColimit