NYLL
Module

GeometricStalkIdempotentDescent.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkIdempotentDescent
7 declarations indexed from sourceView source ↗

Module documentation

Finite idempotent decompositions descend to pointed étale neighborhoods

A finite complete orthogonal family in an arbitrary algebra after base change to the actual geometric stalk descends to one actual pointed étale neighborhood. An affine refinement retains the same idempotents and their literal germ images. All scalar structures are the existing structures on the actual objects under the base ring.

This supplies the finite idempotent descent in external Stacks tag 0BSR, needed for Stacks, Tag 0BST. Prime-fiber finiteness and residue-extension comparisons are separate prerequisites.

Imports13
Imported by2

Declarations

theorem

neighborhoodGerm_naturality

L48 ↗
EtaleFundamentalGroups.StrictHenselian.neighborhoodGerm_naturality
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u w
variable {R : CommRingCat.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)
Lean source · statement
theorem neighborhoodGerm_naturality
    {W V : (Spec R).Etale} (j : V ⟶ W)
    (v : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom φ))).fiber.obj V)
    (t : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom φ))).fiber.obj W)
    (hj : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom φ))).fiber.map j v = t) :
    geometricNeighborhoodAlgebraMap R j ≫ geometricNeighborhoodGerm φ V v =
      geometricNeighborhoodGerm φ W t
theorem

exists_pointed_completeOrthogonalIdempotents

L63 ↗
EtaleFundamentalGroups.StrictHenselian.exists_pointed_completeOrthogonalIdempotents
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u w
variable {R : CommRingCat.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)
Lean source · statement
theorem exists_pointed_completeOrthogonalIdempotents
    {B ι : Type u} [CommRing B] [Algebra R B] [Fintype ι]
    (e : ι → ((geometricStalkSmallAlgebraCocone φ).pt ⊗[R] B))
    (he : CompleteOrthogonalIdempotents e) :
    ∃ (W : (Spec R).Etale)
      (t : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom φ))).fiber.obj W)
      (eW : ι → (geometricNeighborhoodAlgebra R W ⊗[R] B)),
      CompleteOrthogonalIdempotents eW ∧
        ∀ a, Algebra.TensorProduct.map
          (CommRingCat.toAlgHom (geometricNeighborhoodGerm φ W t))
          (AlgHom.id R B) (eW a) = e a
theorem

geometricStalk_exists_affine_completeOrthogonalIdempotents

L85 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalk_exists_affine_completeOrthogonalIdempotents
Documentation

Every finite complete orthogonal family in the actual geometric-stalk base change of an arbitrary algebra descends to an actual affine pointed étale neighborhood, with its prescribed literal germ images.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u w
variable {R : CommRingCat.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)
Lean source · statement
theorem geometricStalk_exists_affine_completeOrthogonalIdempotents
    {B ι : Type u} [CommRing B] [Algebra R B] [Fintype ι]
    (e : ι → ((geometricStalkSmallAlgebraCocone φ).pt ⊗[R] B))
    (he : CompleteOrthogonalIdempotents e) :
    ∃ (V : (Spec R).Etale)
      (v : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom φ))).fiber.obj V),
      IsAffine V.left ∧
        ∃ eV : ι → (geometricNeighborhoodAlgebra R V ⊗[R] B),
          CompleteOrthogonalIdempotents eV ∧
            ∀ a, Algebra.TensorProduct.map
              (CommRingCat.toAlgHom (geometricNeighborhoodGerm φ V v))
              (AlgHom.id R B) (eV a) = e a
instance

coefficientTensorAction

L128 ↗
EtaleFundamentalGroups.StrictHenselian.coefficientTensorAction
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u w
variable {R : CommRingCat.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)
section Equivariant
variable {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

transport_equivariant_family

L132 ↗
EtaleFundamentalGroups.StrictHenselian.transport_equivariant_family
Source context 10 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u w
variable {R : CommRingCat.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)
section Equivariant
variable {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) :=
  Inertia.baseChangeAction R A B G
omit [Finite G] in
Lean source · statement
theorem transport_equivariant_family
    (E A C : Under R) (j : E ⟶ A) (v : A ⟶ C) (t : E ⟶ C) (hcomp : j ≫ v = t)
    {ι : Type u} [Fintype ι] (σ : G →* Equiv.Perm ι)
    (eE : ι → (E ⊗[R] B)) (eC : ι → (C ⊗[R] B))
    (heE : CompleteOrthogonalIdempotents eE)
    (hσ : ∀ (g : G) (a : ι), g • eE a = eE (σ g a))
    (hmap : ∀ a, Algebra.TensorProduct.map (CommRingCat.toAlgHom t)
      (AlgHom.id R B) (eE a) = eC a) :
    ∃ eA : ι → (A ⊗[R] B), CompleteOrthogonalIdempotents eA ∧
      (∀ (g : G) (a : ι), g • eA a = eA (σ g a)) ∧
      ∀ a, Algebra.TensorProduct.map (CommRingCat.toAlgHom v)
        (AlgHom.id R B) (eA a) = eC a
theorem

exists_pointed_equivariant_completeOrthogonalIdempotents

L158 ↗
EtaleFundamentalGroups.StrictHenselian.exists_pointed_equivariant_completeOrthogonalIdempotents
Source context 9 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u w
variable {R : CommRingCat.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)
section Equivariant
variable {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) :=
  Inertia.baseChangeAction R A B G
Lean source · statement
theorem exists_pointed_equivariant_completeOrthogonalIdempotents
    {ι : Type u} [Fintype ι] (σ : G →* Equiv.Perm ι)
    (e : ι → ((geometricStalkSmallAlgebraCocone φ).pt ⊗[R] B))
    (he : CompleteOrthogonalIdempotents e)
    (hσ : ∀ (g : G) (a : ι), g • e a = e (σ g a)) :
    ∃ (W : (Spec R).Etale)
      (t : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom φ))).fiber.obj W)
      (eW : ι → (geometricNeighborhoodAlgebra R W ⊗[R] B)),
      CompleteOrthogonalIdempotents eW ∧
        (∀ (g : G) (a : ι), g • eW a = eW (σ g a)) ∧
        ∀ a, Algebra.TensorProduct.map
          (CommRingCat.toAlgHom (geometricNeighborhoodGerm φ W t))
          (AlgHom.id R B) (eW a) = e a
theorem

geometricStalk_exists_affine_equivariant_completeOrthogonalIdempotents

L183 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalk_exists_affine_equivariant_completeOrthogonalIdempotents
Documentation

A finite complete family in the actual geometric-stalk base change, with a prescribed finite-group permutation action, descends to an actual affine pointed étale neighborhood with the same group equations and the same literal germ images. The acted-on algebra is arbitrary.

Source context 9 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
open scoped TensorProduct
namespace EtaleFundamentalGroups.StrictHenselian
universe u w
variable {R : CommRingCat.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
  (φ : R →+* Ω)
section Equivariant
variable {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) :=
  Inertia.baseChangeAction R A B G
Lean source · statement
theorem geometricStalk_exists_affine_equivariant_completeOrthogonalIdempotents
    {ι : Type u} [Fintype ι] (σ : G →* Equiv.Perm ι)
    (e : ι → ((geometricStalkSmallAlgebraCocone φ).pt ⊗[R] B))
    (he : CompleteOrthogonalIdempotents e)
    (hσ : ∀ (g : G) (a : ι), g • e a = e (σ g a)) :
    ∃ (V : (Spec R).Etale)
      (v : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom φ))).fiber.obj V),
      IsAffine V.left ∧
        ∃ eV : ι → (geometricNeighborhoodAlgebra R V ⊗[R] B),
          CompleteOrthogonalIdempotents eV ∧
            (∀ (g : G) (a : ι), g • eV a = eV (σ g a)) ∧
            ∀ a, Algebra.TensorProduct.map
              (CommRingCat.toAlgHom (geometricNeighborhoodGerm φ V v))
              (AlgHom.id R B) (eV 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.