Module

InvariantFlatBaseChange.lean

Nyll.EtaleFundamentalGroups.Inertia.InvariantFlatBaseChange

11 declarations indexed from sourceView source ↗

Module documentation

Fixed subalgebras commute with flat base change

For a finite group, the fixed subalgebra is the kernel of the linear map r ↦ (g ↦ g • r - r). Flat tensor product preserves this kernel, and tensor product commutes with the finite product indexed by the group. Consequently every invariant tensor comes from the tensor product of the fixed subalgebra.

The resulting algebra equivalence uses the actual action on the second tensor factor and the canonical inclusion of the fixed subalgebra.

Imports5

Nyll.EtaleFundamentalGroups.Inertia.InvariantBaseChange
Mathlib.LinearAlgebra.TensorProduct.Pi
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Invariant.Basic
Mathlib.RingTheory.TensorProduct.Basic

Imported by3

instance

(anonymous instance)

L36 ↗

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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_smulCommClass

L39 ↗

EtaleFundamentalGroups.Inertia.baseChangeAction_smulCommClass

Documentation

The tensor action commutes with scalars from the base-change algebra.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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_smulCommClass : SMulCommClass G A (A ⊗[B] R)

instance

(anonymous instance)

L48 ↗

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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

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

def

actionDifference

L50 ↗

EtaleFundamentalGroups.Inertia.actionDifference

Source context 6 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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
local instance : SMulCommClass G A (A ⊗[B] R) := baseChangeAction_smulCommClass B A R G

Lean source · statement

def actionDifference : R →ₗ[B] (G → R)

theorem

actionDifference_exact

L53 ↗

EtaleFundamentalGroups.Inertia.actionDifference_exact

Source context 6 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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
local instance : SMulCommClass G A (A ⊗[B] R) := baseChangeAction_smulCommClass B A R G

Lean source · statement

theorem actionDifference_exact :
    Function.Exact (FixedPoints.subalgebra B R G).val.toLinearMap
      (actionDifference B R G)

def

invariantTensorHom

L66 ↗

EtaleFundamentalGroups.Inertia.invariantTensorHom

Source context 6 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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
local instance : SMulCommClass G A (A ⊗[B] R) := baseChangeAction_smulCommClass B A R G

Lean source · statement

def invariantTensorHom :
    (A ⊗[B] FixedPoints.subalgebra B R G) →ₐ[A]
      FixedPoints.subalgebra A (A ⊗[B] R) G

theorem

invariantTensorHom_bijective

L80 ↗

EtaleFundamentalGroups.Inertia.invariantTensorHom_bijective

Source context 6 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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
local instance : SMulCommClass G A (A ⊗[B] R) := baseChangeAction_smulCommClass B A R G

Lean source · statement

theorem invariantTensorHom_bijective [Finite G] [Module.Flat B A] :
    Function.Bijective (invariantTensorHom B A R G)

def

invariantFlatBaseChangeEquiv

L115 ↗

EtaleFundamentalGroups.Inertia.invariantFlatBaseChangeEquiv

Documentation

Fixed subalgebras of finite group actions commute with flat base change. The forward map is induced by the inclusion of the original fixed subalgebra.

Source context 6 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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
local instance : SMulCommClass G A (A ⊗[B] R) := baseChangeAction_smulCommClass B A R G

Lean source · statement

def invariantFlatBaseChangeEquiv [Finite G] [Module.Flat B A] :
    (A ⊗[B] FixedPoints.subalgebra B R G) ≃ₐ[A]
      FixedPoints.subalgebra A (A ⊗[B] R) G

theorem

invariantFlatBaseChangeEquiv_val_comp

L122 ↗

EtaleFundamentalGroups.Inertia.invariantFlatBaseChangeEquiv_val_comp

Documentation

The flat base-change equivalence has the canonical inclusion square.

Source context 6 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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
local instance : SMulCommClass G A (A ⊗[B] R) := baseChangeAction_smulCommClass B A R G

Lean source · statement

theorem invariantFlatBaseChangeEquiv_val_comp [Finite G] [Module.Flat B A] :
    (FixedPoints.subalgebra A (A ⊗[B] R) G).val.comp
        (invariantFlatBaseChangeEquiv B A R G).toAlgHom =
      Algebra.TensorProduct.map (AlgHom.id A A) (FixedPoints.subalgebra B R G).val

theorem

baseChangeAction_isInvariant

L132 ↗

EtaleFundamentalGroups.Inertia.baseChangeAction_isInvariant

Documentation

If the original fixed elements are exactly the image of the base, the same holds after flat base change. The proof uses the actual fixed-subalgebra base-change equivalence and its canonical inclusion square.

Source context 6 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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
local instance : SMulCommClass G A (A ⊗[B] R) := baseChangeAction_smulCommClass B A R G

Lean source · statement

theorem baseChangeAction_isInvariant [Finite G] [Module.Flat B A]
    [Algebra.IsInvariant B R G] : Algebra.IsInvariant A (A ⊗[B] R) G

theorem

baseChangeAction_finite_primesOver

L153 ↗

EtaleFundamentalGroups.Inertia.baseChangeAction_finite_primesOver

Documentation

Every prime fiber after flat base change of a finite invariant action is finite. A nonempty fiber is the orbit of any one of its actual primes.

Source context 6 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped TensorProduct Pointwise
universe u v w z
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
local instance : SMulCommClass G A (A ⊗[B] R) := baseChangeAction_smulCommClass B A R G

Lean source · statement

theorem baseChangeAction_finite_primesOver [Finite G] [Module.Flat B A]
    [Algebra.IsInvariant B R G] (p : Ideal A) :
    (p.primesOver (A ⊗[B] R)).Finite

Module documentation

Fixed subalgebras commute with flat base change

Declarations