Module

InvariantEtaleFactorNeighborhood.lean

Nyll.EtaleFundamentalGroups.Inertia.InvariantEtaleFactorNeighborhood

9 declarations indexed from sourceView source ↗

Module documentation

The actual étale neighborhood map from an invariant tensor factor

The existing flat invariant equivalence identifies the base-changed original fixed algebra with the fixed tensor algebra. Its composition with the right tensor inclusion and a principal localization gives the actual neighborhood map to the original fixed algebra. Étaleness follows from canonical base change, the existing equivalence, and principal localization. The literal square over the original base is retained.

For the finite transitive idempotent family, the previously constructed coefficient-to-factor bijection additionally identifies this neighborhood with the coefficient scheme. Source-local descent from its open image is a separate step in Stacks tag 0BST.

Imports13

Nyll.EtaleFundamentalGroups.Inertia.InvariantBaseChange
Nyll.EtaleFundamentalGroups.Inertia.InvariantFlatBaseChange
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.RingHom.Etale
Mathlib.RingTheory.RingHomProperties
Mathlib.RingTheory.TensorProduct.Maps
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.RingTheory.Spectrum.Prime.RingHom
Mathlib.RingTheory.Ideal.Maps

Imported by2

theorem

tensorIncludeRight_etale

L47 ↗

EtaleFundamentalGroups.Inertia.tensorIncludeRight_etale

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped TensorProduct
namespace EtaleFundamentalGroups.Inertia
universe u w

Lean source · statement

theorem tensorIncludeRight_etale
    (B A S : Type u) [CommRing B] [CommRing A] [CommRing S]
    [Algebra B A] [Algebra B S] [Algebra.Etale B A] :
    (Algebra.TensorProduct.includeRight (R := B) (A := A) (B := S)).toRingHom.Etale

instance

(anonymous instance)

L59 ↗

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped TensorProduct
namespace EtaleFundamentalGroups.Inertia
universe u w
variable (B A R : Type u) (G : Type w)
  [CommRing B] [CommRing A] [CommRing R] [Algebra B A] [Algebra B R]
  [Group G] [Finite G] [MulSemiringAction G R] [SMulCommClass G B R]

Lean source · statement

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

instance

(anonymous instance)

L60 ↗

Source context 7 commands

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

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

Lean source · statement

instance : SMulCommClass G A (A ⊗[B] R)

def

invariantFlatBaseChangeFactorMap

L64 ↗

EtaleFundamentalGroups.Inertia.invariantFlatBaseChangeFactorMap

Documentation

The literal map from the original fixed algebra into a localized fixed factor after flat base change. It uses the existing invariant equivalence.

Source context 8 commands

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

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

Lean source · statement

def invariantFlatBaseChangeFactorMap [Module.Flat B A]
    (e : FixedPoints.subalgebra A (A ⊗[B] R) G) :
    FixedPoints.subalgebra B R G →+* Localization.Away e

theorem

invariantFlatBaseChangeFactorMap_etale

L74 ↗

EtaleFundamentalGroups.Inertia.invariantFlatBaseChangeFactorMap_etale

Documentation

An étale coefficient extension makes the actual selected-factor neighborhood map étale, including finite presentation.

Source context 8 commands

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

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

Lean source · statement

theorem invariantFlatBaseChangeFactorMap_etale [Algebra.Etale B A]
    (e : FixedPoints.subalgebra A (A ⊗[B] R) G) :
    RingHom.Etale (R := FixedPoints.subalgebra B R G) (S := Localization.Away e)
      (invariantFlatBaseChangeFactorMap B A R G e)

theorem

invariantFactorNeighborhood_etale

L86 ↗

EtaleFundamentalGroups.Inertia.invariantFactorNeighborhood_etale

Documentation

The actual scheme map from the selected factor to the original fixed algebra is an étale neighborhood map.

Source context 8 commands

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

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

Lean source · statement

theorem invariantFactorNeighborhood_etale [Algebra.Etale B A]
    (e : FixedPoints.subalgebra A (A ⊗[B] R) G) :
    Etale (Spec.map (CommRingCat.ofHom (R := FixedPoints.subalgebra B R G)
      (S := Localization.Away e)
      (invariantFlatBaseChangeFactorMap B A R G e)))

theorem

invariantFlatBaseChangeFactorMap_comp_algebraMap

L96 ↗

EtaleFundamentalGroups.Inertia.invariantFlatBaseChangeFactorMap_comp_algebraMap

Documentation

The neighborhood map preserves the literal original base map, through the prescribed coefficient action on the localized factor.

Source context 8 commands

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

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

Lean source · statement

theorem invariantFlatBaseChangeFactorMap_comp_algebraMap [Module.Flat B A]
    (e : FixedPoints.subalgebra A (A ⊗[B] R) G) :
    (invariantFlatBaseChangeFactorMap B A R G e).comp
        (algebraMap B (FixedPoints.subalgebra B R G)) =
      (algebraMap A (Localization.Away e)).comp (algebraMap B A)

theorem

invariantFactorNeighborhood_square

L117 ↗

EtaleFundamentalGroups.Inertia.invariantFactorNeighborhood_square

Documentation

The selected-factor neighborhood has its literal compatibility square with the coefficient scheme and the original base scheme.

Source context 8 commands

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

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

Lean source · statement

theorem invariantFactorNeighborhood_square [Module.Flat B A]
    (e : FixedPoints.subalgebra A (A ⊗[B] R) G) :
    Spec.map (CommRingCat.ofHom (R := FixedPoints.subalgebra B R G) (S := Localization.Away e)
      (invariantFlatBaseChangeFactorMap B A R G e)) ≫
        Spec.map (CommRingCat.ofHom (algebraMap B (FixedPoints.subalgebra B R G))) =
      Spec.map (CommRingCat.ofHom (R := A) (S := Localization.Away e)
        (algebraMap A (Localization.Away e))) ≫
        Spec.map (CommRingCat.ofHom (algebraMap B A))

theorem

invariantFactorNeighborhood_exists_point

L133 ↗

EtaleFundamentalGroups.Inertia.invariantFactorNeighborhood_exists_point

Documentation

A prime of the tensor algebra outside the selected element supplies an actual point of the localized invariant neighborhood. Its contraction is exactly the contraction of the original ring prime to its invariant algebra.

Source context 8 commands

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

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

Lean source · statement

theorem invariantFactorNeighborhood_exists_point [Module.Flat B A]
    (Q : PrimeSpectrum (A ⊗[B] R))
    (e : FixedPoints.subalgebra A (A ⊗[B] R) G) (he : (e : A ⊗[B] R) ∉ Q.asIdeal) :
    ∃ P : PrimeSpectrum (Localization.Away e),
      PrimeSpectrum.comap (R := FixedPoints.subalgebra B R G) (S := Localization.Away e)
          (invariantFlatBaseChangeFactorMap B A R G e) P =
        PrimeSpectrum.comap
          ((Algebra.TensorProduct.includeRight (R := B) (A := A) (B := R)).toRingHom.comp
            (FixedPoints.subalgebra B R G).val.toRingHom) Q

Module documentation

The actual étale neighborhood map from an invariant tensor factor

Declarations