Module

InvariantBaseChange.lean

Nyll.EtaleFundamentalGroups.Inertia.InvariantBaseChange

6 declarations indexed from sourceView source ↗

Module documentation

Inertia under base change

The action on the second tensor factor preserves inertia at every ideal and its contraction. In particular, this proves Stacks Project, Tag 0BSS for arbitrary base change from the fixed subring. No finiteness or primality is needed for this ideal-theoretic statement.

Reference: https://stacks.math.columbia.edu/tag/0BSS

Imports3

Mathlib.Algebra.Algebra.Subalgebra.Operations
Mathlib.RingTheory.Ideal.Defs
Mathlib.RingTheory.TensorProduct.Maps

Imported by6

abbrev

baseChangeAction

L36 ↗

EtaleFundamentalGroups.Inertia.baseChangeAction

Documentation

Extend a ring action, fixing the base, to the second tensor factor.

Source context 5 commands

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

open scoped TensorProduct
namespace EtaleFundamentalGroups.Inertia
universe u v w z
section BaseChange
variable (B : Type u) (A : Type v) (R : Type w) (G : Type z)
  [CommRing B] [CommRing A] [CommRing R] [Algebra B A] [Algebra B R]
  [Group G] [MulSemiringAction G R] [SMulCommClass G B R]

Lean source · statement

abbrev baseChangeAction : MulSemiringAction G (A ⊗[B] R)

instance

(anonymous instance)

L62 ↗

Source context 5 commands

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

open scoped TensorProduct
namespace EtaleFundamentalGroups.Inertia
universe u v w z
section BaseChange
variable (B : Type u) (A : Type v) (R : Type w) (G : Type z)
  [CommRing B] [CommRing A] [CommRing R] [Algebra B A] [Algebra B R]
  [Group G] [MulSemiringAction G R] [SMulCommClass G B R]

Lean source · statement

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

theorem

baseChangeAction_tmul

L65 ↗

EtaleFundamentalGroups.Inertia.baseChangeAction_tmul

Documentation

The extended action fixes the first tensor factor.

Source context 6 commands

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

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

Lean source · statement

theorem baseChangeAction_tmul (g : G) (a : A) (r : R) :
    g • (a ⊗ₜ[B] r) = a ⊗ₜ[B] (g • r)

theorem

inertia_comap_includeRight

L72 ↗

EtaleFundamentalGroups.Inertia.inertia_comap_includeRight

Documentation

Inertia is unchanged by tensor base change, at any ideal and its contraction to the acted-on factor.

Source context 6 commands

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

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

Lean source · statement

theorem inertia_comap_includeRight (Q : Ideal (A ⊗[B] R)) :
    (Q.comap (Algebra.TensorProduct.includeRight (R := B) (A := A)
      (B := R)).toRingHom).inertia G = Q.inertia G

theorem

baseChangeAction_map

L97 ↗

EtaleFundamentalGroups.Inertia.baseChangeAction_map

Documentation

The prescribed action on the fixed tensor factor commutes with an actual change of the coefficient algebra. This is the existing tensor-map composition identity applied to the two independent coordinates.

Source context 6 commands

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

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

Lean source · full declaration

theorem baseChangeAction_map {A' : Type*} [CommRing A'] [Algebra B A']
    (f : A →ₐ[B] A') :
    let : MulSemiringAction G (A' ⊗[B] R) := baseChangeAction B A' R G
    ∀ (g : G) (x : A ⊗[B] R),
      Algebra.TensorProduct.map f (AlgHom.id B R) (g • x) =
        g • Algebra.TensorProduct.map f (AlgHom.id B R) x := by
  intro targetAction g x
  change Algebra.TensorProduct.map f (AlgHom.id B R)
      (Algebra.TensorProduct.map (AlgHom.id B A) (MulSemiringAction.toAlgHom B R g) x) =
    Algebra.TensorProduct.map (AlgHom.id B A') (MulSemiringAction.toAlgHom B R g)
      (Algebra.TensorProduct.map f (AlgHom.id B R) x)
  have h :
      (Algebra.TensorProduct.map f (AlgHom.id B R)).comp
          (Algebra.TensorProduct.map (AlgHom.id B A) (MulSemiringAction.toAlgHom B R g)) =
        (Algebra.TensorProduct.map (AlgHom.id B A') (MulSemiringAction.toAlgHom B R g)).comp
          (Algebra.TensorProduct.map f (AlgHom.id B R)) := by
    rw [← Algebra.TensorProduct.map_comp, ← Algebra.TensorProduct.map_comp]
    simp only [AlgHom.id_comp, AlgHom.comp_id]
  exact AlgHom.congr_fun h x

theorem

inertia_invariantBaseChange

L122 ↗

EtaleFundamentalGroups.Inertia.inertia_invariantBaseChange

Documentation

Stacks Project, Tag 0BSS: a base change from the invariant subring preserves the inertia group at each prime (and, more generally, each ideal). The tensor action is constructed from the given action on R.

Source context 3 commands

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

open scoped TensorProduct
namespace EtaleFundamentalGroups.Inertia
universe u v w z

Lean source · full declaration

theorem inertia_invariantBaseChange
    (A : Type v) (R : Type w) (G : Type z)
    [CommRing A] [CommRing R] [Group G] [MulSemiringAction G R]
    [Algebra (FixedPoints.subring R G) A]
    (Q : Ideal (A ⊗[FixedPoints.subring R G] R)) :
    letI := baseChangeAction (FixedPoints.subring R G) A R G
    (Q.comap (Algebra.TensorProduct.includeRight
      (R := FixedPoints.subring R G) (A := A) (B := R)).toRingHom).inertia G =
      Q.inertia G :=
  inertia_comap_includeRight (FixedPoints.subring R G) A R G Q

Module documentation

Inertia under base change

Declarations

baseChangeAction

(anonymous instance)

baseChangeAction_tmul

inertia_comap_includeRight

baseChangeAction_map

inertia_invariantBaseChange