Module

NativeAlgebraResidueEpi.lean

Nyll.SchemeTheory.RingTheory.Ramification.NativeAlgebraResidueEpi

12 declarations indexed from sourceView source ↗

Module documentation

The native residue epimorphism from an actual algebra object

The coefficient map and its action are those stored in the native algebra object. Coefficient fixedness, fixed-element descent, and open stabilizers supply the actual compact residue-lift theorem. Its surjectivity proves a categorical epimorphism; none of these conclusions are input data.

Imports4

Nyll.SchemeTheory.CategoryTheory.CommAlgRingMap
Nyll.SchemeTheory.RingTheory.Ramification.NativeResidueAction
Mathlib.Algebra.Category.Grp.EpiMono
Mathlib.Topology.Algebra.MulAction

Imported by6

theorem

nativeGroupMorphism_epi_of_surjective

L30 ↗

EtaleFundamentalGroups.Inertia.nativeGroupMorphism_epi_of_surjective

Documentation

The ordinary group-category implication, with coercions confined to groups.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

theorem nativeGroupMorphism_epi_of_surjective {D H : GrpCat.{v}}
    (f : GrpCat.Hom D H) (hf : Function.Surjective f.hom'.toFun) :
    Epi (C := GrpCat.{v}) (X := D) (Y := H) f

theorem

nativeGroupMorphism_surjective_of_epi

L36 ↗

EtaleFundamentalGroups.Inertia.nativeGroupMorphism_surjective_of_epi

Documentation

The converse uses the existing native group-category theorem.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

theorem nativeGroupMorphism_surjective_of_epi {D H : GrpCat.{v}}
    (f : GrpCat.Hom D H) [Epi (C := GrpCat.{v}) (X := D) (Y := H) f] :
    Function.Surjective f.hom'.toFun

theorem

coefficientFixed_smulCommClass

L41 ↗

EtaleFundamentalGroups.Inertia.coefficientFixed_smulCommClass

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

theorem coefficientFixed_smulCommClass
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (G : Type v) [Group G] [MulSemiringAction G R]
    (hbase : ∀ g : G, (MulSemiringAction.toRingHom G R g).comp
      (commAlgCoefficientMap R) = commAlgCoefficientMap R) : SMulCommClass G A R

theorem

fixedCoefficient_isInvariant

L52 ↗

EtaleFundamentalGroups.Inertia.fixedCoefficient_isInvariant

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

theorem fixedCoefficient_isInvariant
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (G : Type v) [Group G] [MulSemiringAction G R]
    (hinv : ∀ b : R, (∀ g : G, g • b = b) →
      ∃ a : A, (commAlgCoefficientMap R).toFun a = b) : Algebra.IsInvariant A R G

theorem

fixedSet_continuousSMul

L61 ↗

EtaleFundamentalGroups.Inertia.fixedSet_continuousSMul

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · full declaration

theorem fixedSet_continuousSMul
    {G X : Type v} [Group G] [MulAction G X]
    [TopologicalSpace G] [IsTopologicalGroup G]
    [TopologicalSpace X] [DiscreteTopology X]
    (hopen : ∀ x : X, IsOpen (fun g : G => g • x = x)) : ContinuousSMul G X :=
  continuousSMul_iff_stabilizer_isOpen.mpr hopen

def

nativeAlgebraResidueBaseIdeal

L69 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueBaseIdeal

Documentation

The actual contraction along the stored native coefficient map.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

def nativeAlgebraResidueBaseIdeal {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (q : Ideal R) : Ideal A

theorem

nativeAlgebraResidueBaseIdeal_liesOver

L72 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueBaseIdeal_liesOver

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

theorem nativeAlgebraResidueBaseIdeal_liesOver
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A) (q : Ideal R) :
    q.LiesOver (nativeAlgebraResidueBaseIdeal R q)

def

nativeAlgebraResidueAutomorphisms

L79 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueAutomorphisms

Documentation

The actual quotient-algebra automorphism group over the contracted prime.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

def nativeAlgebraResidueAutomorphisms {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (q : Ideal R) : GrpCat.{v}

def

nativeAlgebraResidueMorphism

L86 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueMorphism

Documentation

The literal native residue-action map for the stored coefficient action.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

def nativeAlgebraResidueMorphism {A : Type u} [CommRing A]
    (R : CommAlgCat.{v} A) (G : Type v) [Group G] [MulSemiringAction G R]
    (q : Ideal R)
    (hbase : ∀ g : G, (MulSemiringAction.toRingHom G R g).comp
      (commAlgCoefficientMap R) = commAlgCoefficientMap R) :
    GrpCat.Hom (nativeResidueStabilizer R G q) (nativeAlgebraResidueAutomorphisms R q)

theorem

nativeAlgebraResidueMorphism_epi

L98 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueMorphism_epi

Documentation

The actual residue map is epic, by the proved compact residue lift.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · full declaration

theorem nativeAlgebraResidueMorphism_epi
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (G : Type v) [Group G] [MulSemiringAction G R]
    [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G]
    [IsTopologicalGroup G] (q : Ideal R) [q.IsPrime]
    (hbase : ∀ g : G, (MulSemiringAction.toRingHom G R g).comp
      (commAlgCoefficientMap R) = commAlgCoefficientMap R)
    (hinv : ∀ b : R, (∀ g : G, g • b = b) →
      ∃ a : A, (commAlgCoefficientMap R).toFun a = b)
    (hopen : ∀ b : R, IsOpen (fun g : G => g • b = b)) :
    Epi (C := GrpCat.{v}) (X := nativeResidueStabilizer R G q)
      (Y := nativeAlgebraResidueAutomorphisms R q)
      (nativeAlgebraResidueMorphism R G q hbase) := by
  have : SMulCommClass G A R := coefficientFixed_smulCommClass R G hbase
  have : Algebra.IsInvariant A R G := fixedCoefficient_isInvariant R G hinv
  let : TopologicalSpace R := ⊥
  have : DiscreteTopology R := ⟨rfl⟩
  have : ContinuousSMul G R := fixedSet_continuousSMul hopen
  have : q.LiesOver (nativeAlgebraResidueBaseIdeal R q) :=
    nativeAlgebraResidueBaseIdeal_liesOver R q
  apply nativeGroupMorphism_epi_of_surjective
  change Function.Surjective
    (nativeResidueStabilizerHom A R G (nativeAlgebraResidueBaseIdeal R q) q).toFun
  exact nativeResidueStabilizerHom_surjective A R G (nativeAlgebraResidueBaseIdeal R q) q

def

nativeAlgebraResidueKernelImage

L124 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueKernelImage

Documentation

The image in the original group of the actual residue-map kernel.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

def nativeAlgebraResidueKernelImage
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (G : Type v) [Group G] [MulSemiringAction G R] (q : Ideal R)
    (hbase : ∀ g : G, (MulSemiringAction.toRingHom G R g).comp
      (commAlgCoefficientMap R) = commAlgCoefficientMap R) : Subgroup G

theorem

nativeAlgebraResidueKernelImage_eq_inertia

L133 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueKernelImage_eq_inertia

Documentation

The computed kernel image is the literal native inertia subgroup.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory CategoryTheory
universe u v

Lean source · statement

theorem nativeAlgebraResidueKernelImage_eq_inertia
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (G : Type v) [Group G] [MulSemiringAction G R] (q : Ideal R)
    (hbase : ∀ g : G, (MulSemiringAction.toRingHom G R g).comp
      (commAlgCoefficientMap R) = commAlgCoefficientMap R) :
    nativeAlgebraResidueKernelImage R G q hbase = q.inertia G

Module documentation

The native residue epimorphism from an actual algebra object

Declarations