Module

FiniteInvariantResidueLift.lean

Nyll.SchemeTheory.RingTheory.Ramification.FiniteInvariantResidueLift

12 declarations indexed from sourceView source ↗

Module documentation

Finite invariant residue lifts through native ring maps

The finite characteristic-polynomial theorem proves preservation of the actual coefficient image. The native first isomorphism theorem transports the resulting image automorphism to the quotient by the kernel. The native finite stabilizer surjection then gives one group element satisfying all coefficient equations. No algebra from that kernel quotient to the target ring is introduced.

Imports6

Nyll.SchemeTheory.RingTheory.Ramification.FiniteInvariantRingImage
Mathlib.Algebra.Ring.Subring.Basic
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Invariant.Basic

Imported by2

theorem

inverse_fixes_coefficient

L29 ↗

EtaleFundamentalGroups.Inertia.inverse_fixes_coefficient

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem inverse_fixes_coefficient
    {A T : Type*} [CommRing A] [CommRing T]
    (φ : T ≃+* T) (a : A →+* T) (h : φ.toRingHom.comp a = a) :
    φ.symm.toRingHom.comp a = a

theorem

image_mem_iff

L39 ↗

EtaleFundamentalGroups.Inertia.image_mem_iff

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem image_mem_iff
    {C T : Type*} [CommRing C] [CommRing T]
    (f : C →+* T) (φ : T ≃+* T)
    (hf : ∀ x : C, ∃ y : C, f.toFun y = φ.toRingHom.toFun (f.toFun x))
    (hb : ∀ x : C, ∃ y : C, f.toFun y = φ.symm.toRingHom.toFun (f.toFun x)) :
    ∀ x : T, x ∈ f.range ↔ φ.toRingHom.toFun x ∈ f.range

theorem

quotientKerEquivRange_coefficient

L54 ↗

EtaleFundamentalGroups.Inertia.quotientKerEquivRange_coefficient

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem quotientKerEquivRange_coefficient
    {C T : Type*} [CommRing C] [CommRing T]
    (f : C →+* T) (x : C ⧸ RingHom.ker f) :
    ((f.quotientKerEquivRange.toRingHom.toFun x : f.range) : T) =
      (RingHom.kerLift f).toFun x

def

imageQuotientEquiv

L66 ↗

EtaleFundamentalGroups.Inertia.imageQuotientEquiv

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

def imageQuotientEquiv
    {C T : Type*} [CommRing C] [CommRing T]
    (f : C →+* T) (φ : T ≃+* T)
    (hf : ∀ x : C, ∃ y : C, f.toFun y = φ.toRingHom.toFun (f.toFun x))
    (hb : ∀ x : C, ∃ y : C, f.toFun y = φ.symm.toRingHom.toFun (f.toFun x)) :
    (C ⧸ RingHom.ker f) ≃+* (C ⧸ RingHom.ker f)

theorem

imageQuotientEquiv_comp

L76 ↗

EtaleFundamentalGroups.Inertia.imageQuotientEquiv_comp

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem imageQuotientEquiv_comp
    {C T : Type*} [CommRing C] [CommRing T]
    (f : C →+* T) (φ : T ≃+* T)
    (hf : ∀ x : C, ∃ y : C, f.toFun y = φ.toRingHom.toFun (f.toFun x))
    (hb : ∀ x : C, ∃ y : C, f.toFun y = φ.symm.toRingHom.toFun (f.toFun x)) :
    (RingHom.kerLift f).comp (imageQuotientEquiv f φ hf hb).toRingHom =
      φ.toRingHom.comp (RingHom.kerLift f)

def

imageQuotientAlgEquiv

L97 ↗

EtaleFundamentalGroups.Inertia.imageQuotientAlgEquiv

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · full declaration

def imageQuotientAlgEquiv
    {A C T : Type*} [CommRing A] [CommRing C] [CommRing T] [Algebra A C]
    (f : C →+* T) (φ : T ≃+* T)
    (hf : ∀ x : C, ∃ y : C, f.toFun y = φ.toRingHom.toFun (f.toFun x))
    (hb : ∀ x : C, ∃ y : C, f.toFun y = φ.symm.toRingHom.toFun (f.toFun x))
    (hφ : φ.toRingHom.comp (f.comp (algebraMap A C)) = f.comp (algebraMap A C)) :
    (C ⧸ RingHom.ker f) ≃ₐ[A ⧸ (RingHom.ker f).under A] (C ⧸ RingHom.ker f) where
  toRingEquiv := imageQuotientEquiv f φ hf hb
  commutes' z := by
    obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective z
    change (imageQuotientEquiv f φ hf hb).toRingHom.toFun
        ((Ideal.Quotient.mk (RingHom.ker f)).toFun ((algebraMap A C).toFun a)) =
      (Ideal.Quotient.mk (RingHom.ker f)).toFun ((algebraMap A C).toFun a)
    apply RingHom.kerLift_injective f
    have he := congrArg (fun g : (C ⧸ RingHom.ker f) →+* T =>
        g.toFun ((Ideal.Quotient.mk (RingHom.ker f)).toFun ((algebraMap A C).toFun a)))
      (imageQuotientEquiv_comp f φ hf hb)
    have ha := congrArg (fun g : A →+* T => g.toFun a) hφ
    exact he.trans ((congrArg φ.toRingHom.toFun
      (RingHom.kerLift_mk f ((algebraMap A C).toFun a))).trans
        (ha.trans (RingHom.kerLift_mk f ((algebraMap A C).toFun a)).symm))

theorem

finiteInvariantImage_forward

L119 ↗

EtaleFundamentalGroups.Inertia.finiteInvariantImage_forward

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem finiteInvariantImage_forward
    {A C T H : Type*} [CommRing A] [CommRing C] [CommRing T] [IsDomain T]
    [Algebra A C] [Group H] [Finite H] [MulSemiringAction H C]
    [Algebra.IsInvariant A C H]
    (f : C →+* T) (φ : T ≃+* T)
    (hφ : φ.toRingHom.comp (f.comp (algebraMap A C)) = f.comp (algebraMap A C)) :
    ∀ x : C, ∃ y : C, f.toFun y = φ.toRingHom.toFun (f.toFun x)

def

finiteInvariantImageQuotientAlgEquiv

L130 ↗

EtaleFundamentalGroups.Inertia.finiteInvariantImageQuotientAlgEquiv

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

def finiteInvariantImageQuotientAlgEquiv
    {A C T H : Type*} [CommRing A] [CommRing C] [CommRing T] [IsDomain T]
    [Algebra A C] [Group H] [Finite H] [MulSemiringAction H C]
    [Algebra.IsInvariant A C H]
    (f : C →+* T) (φ : T ≃+* T)
    (hφ : φ.toRingHom.comp (f.comp (algebraMap A C)) = f.comp (algebraMap A C)) :
    (C ⧸ RingHom.ker f) ≃ₐ[A ⧸ (RingHom.ker f).under A] (C ⧸ RingHom.ker f)

theorem

finiteInvariantImageQuotientAlgEquiv_comp

L142 ↗

EtaleFundamentalGroups.Inertia.finiteInvariantImageQuotientAlgEquiv_comp

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem finiteInvariantImageQuotientAlgEquiv_comp
    {A C T H : Type*} [CommRing A] [CommRing C] [CommRing T] [IsDomain T]
    [Algebra A C] [Group H] [Finite H] [MulSemiringAction H C]
    [Algebra.IsInvariant A C H]
    (f : C →+* T) (φ : T ≃+* T)
    (hφ : φ.toRingHom.comp (f.comp (algebraMap A C)) = f.comp (algebraMap A C)) :
    (RingHom.kerLift f).comp (finiteInvariantImageQuotientAlgEquiv (H := H) f φ hφ).toRingHom =
      φ.toRingHom.comp (RingHom.kerLift f)

theorem

finiteInvariantQuotient_exists_lift

L155 ↗

EtaleFundamentalGroups.Inertia.finiteInvariantQuotient_exists_lift

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem finiteInvariantQuotient_exists_lift
    {A C : Type*} [CommRing A] [CommRing C] [Algebra A C]
    (H : Type*) [Group H] [Finite H] [MulSemiringAction H C]
    [SMulCommClass H A C] [Algebra.IsInvariant A C H]
    (p : Ideal A) (q : Ideal C) [q.IsPrime] [q.LiesOver p]
    (σ : (C ⧸ q) ≃ₐ[A ⧸ p] (C ⧸ q)) :
    ∃ h : H, ∀ c : C, (Ideal.Quotient.mk q).toFun (h • c) =
      σ.toRingHom.toFun ((Ideal.Quotient.mk q).toFun c)

theorem

ringHomKernel_isPrime

L169 ↗

EtaleFundamentalGroups.Inertia.ringHomKernel_isPrime

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem ringHomKernel_isPrime
    {C T : Type*} [CommRing C] [CommRing T] [IsDomain T] (f : C →+* T) :
    (RingHom.ker f).IsPrime

theorem

finiteInvariantRingHom_exists_lift

L177 ↗

EtaleFundamentalGroups.Inertia.finiteInvariantRingHom_exists_lift

Documentation

For a finite invariant action, a target automorphism fixing the original coefficient map lifts to one group element on the entire coefficient image. The conclusion is an equation in the target ring for each original element.

Source context 2 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia

Lean source · statement

theorem finiteInvariantRingHom_exists_lift
    {A C T H : Type*} [CommRing A] [CommRing C] [CommRing T] [IsDomain T]
    [Algebra A C] [Group H] [Finite H] [MulSemiringAction H C]
    [SMulCommClass H A C] [Algebra.IsInvariant A C H]
    (f : C →+* T) (φ : T ≃+* T)
    (hφ : φ.toRingHom.comp (f.comp (algebraMap A C)) = f.comp (algebraMap A C)) :
    ∃ h : H, ∀ c : C, f.toFun (h • c) = φ.toRingHom.toFun (f.toFun c)

Module documentation

Finite invariant residue lifts through native ring maps

Declarations