NYLL
Module

IdempotentDescent.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.IdempotentDescent
3 declarations indexed from sourceView source ↗

Module documentation

Descent of a finite complete family of tensor idempotents

A complete orthogonal family determines a map from a finite product of the base ring. The existing finite-presentation descent theorem descends that map. Its values on the standard idempotents give the required family, with the original literal cocone images. The other tensor factor is arbitrary.

This is finite idempotent data needed by the external Stacks tag 0BSR. It does not assert that prime fibers or their residue extensions have descended.

Imports8
Imported by3

Declarations

def

completeOrthogonalIdempotentsAlgHom

L38 ↗
EtaleFundamentalGroups.completeOrthogonalIdempotentsAlgHom
Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
Lean source · full declaration
def completeOrthogonalIdempotentsAlgHom
    {R A ι : Type u} [CommRing R] [CommRing A] [Algebra R A] [Fintype ι]
    {e : ι → A} (he : CompleteOrthogonalIdempotents e) : (ι → R) →ₐ[R] A where
  __ := he.ringEquivOfComm.symm.toRingHom.comp
    (RingHom.pi fun i =>
      ((Pi.evalRingHom (fun j => (he.idem j).Corner) i).comp
        (he.ringEquivOfComm.toRingHom.comp (algebraMap R A))).comp
          (Pi.evalRingHom (fun _ : ι => R) i))
  commutes' r := by
    apply he.ringEquivOfComm.injective
    change he.ringEquivOfComm (he.ringEquivOfComm.symm _) = _
    rw [he.ringEquivOfComm.apply_symm_apply]
    rfl
theorem

completeOrthogonalIdempotentsAlgHom_single

L52 ↗
EtaleFundamentalGroups.completeOrthogonalIdempotentsAlgHom_single
Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem completeOrthogonalIdempotentsAlgHom_single
    {R A ι : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Fintype ι] [DecidableEq ι]
    {e : ι → A} (he : CompleteOrthogonalIdempotents e) (i : ι) :
    completeOrthogonalIdempotentsAlgHom (R := R) he (Pi.single i 1) = e i
theorem

exists_completeOrthogonalIdempotents_stage_of_filteredColimit

L71 ↗
EtaleFundamentalGroups.exists_completeOrthogonalIdempotents_stage_of_filteredColimit
Documentation

A finite complete orthogonal family after base change to a filtered colimit already occurs at a stage. No finiteness hypothesis is imposed on the fixed tensor factor, and each idempotent retains its given cocone image.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem exists_completeOrthogonalIdempotents_stage_of_filteredColimit
    {R : CommRingCat.{u}} {B : Type u} [CommRing B] [Algebra R B]
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under R) (c : Cocone F) (hc : IsColimit c)
    {ι : Type u} [Fintype ι]
    (e : ι → (c.pt ⊗[R] B)) (he : CompleteOrthogonalIdempotents e) :
    ∃ (i : J) (eᵢ : ι → (F.obj i ⊗[R] B)),
      CompleteOrthogonalIdempotents eᵢ ∧
        ∀ a, filteredTensorToColimitAlgHom c i (eᵢ a) = e a

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.