NYLL
Module

FiniteFixedResidueLift.lean

Nyll.SchemeTheory.RingTheory.Ramification.FiniteFixedResidueLift
20 declarations indexed from sourceView source ↗

Module documentation

Finite quotient lifts expressed in the original residue ring

The native quotient action is first constructed on the fixed subring before introducing a coefficient algebra. Its literal carrier is then the existing fixed subalgebra over the original base. The finite uniform-lift theorem produces equations directly in the original quotient B/q on N-fixed elements of B. No fixed-ring quotient or residue algebra over such a quotient is used.

Imports8
Imported by2

Declarations

def

fixedSubringNative

L34 ↗
EtaleFundamentalGroups.Inertia.fixedSubringNative
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
def fixedSubringNative (B : Type v) (G : Type w)
    [CommRing B] [Group G] [MulSemiringAction G B] (N : Subgroup G) :
    CommRingCat.{v}
abbrev

fixedSubringQuotientAction

L39 ↗
EtaleFundamentalGroups.Inertia.fixedSubringQuotientAction
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
abbrev fixedSubringQuotientAction (B : Type v) (G : Type w)
    [CommRing B] [Group G] [MulSemiringAction G B] (N : Subgroup G) [N.Normal] :
    MulSemiringAction (G ⧸ N) (fixedSubringNative B G N)
def

fixedAlgebraNative

L49 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraNative
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
Lean source · statement
def fixedAlgebraNative : CommAlgCat.{v} A
def

fixedAlgebraInclusion

L52 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraInclusion
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
Lean source · statement
def fixedAlgebraInclusion : fixedAlgebraNative A B G N →+* B
theorem

fixedAlgebraInclusion_injective

L55 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraInclusion_injective
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
Lean source · statement
theorem fixedAlgebraInclusion_injective :
    Function.Injective (fixedAlgebraInclusion A B G N).toFun
def

fixedAlgebraBaseMap

L59 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraBaseMap
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
Lean source · statement
def fixedAlgebraBaseMap : A →+* fixedAlgebraNative A B G N
theorem

fixedAlgebraBaseMap_eq_algebraMap

L62 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraBaseMap_eq_algebraMap
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
Lean source · statement
theorem fixedAlgebraBaseMap_eq_algebraMap :
    fixedAlgebraBaseMap A B G N = algebraMap A (fixedAlgebraNative A B G N)
theorem

fixedAlgebraInclusion_comp_base

L66 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraInclusion_comp_base
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
Lean source · statement
theorem fixedAlgebraInclusion_comp_base :
    (fixedAlgebraInclusion A B G N).comp (fixedAlgebraBaseMap A B G N) =
      algebraMap A B
def

fixedAlgebraInclusionAlgHom

L71 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraInclusionAlgHom
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
Lean source · full declaration
def fixedAlgebraInclusionAlgHom : fixedAlgebraNative A B G N →ₐ[A] B where
  toRingHom := fixedAlgebraInclusion A B G N
  commutes' a := by
    have h : (fixedAlgebraInclusion A B G N).comp
        (algebraMap A (fixedAlgebraNative A B G N)) = algebraMap A B := by
      rw [← fixedAlgebraBaseMap_eq_algebraMap A B G N]
      exact fixedAlgebraInclusion_comp_base A B G N
    exact congrArg (fun f : A →+* B => f.toFun a) h
theorem

fixedAlgebraInclusion_smul

L80 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraInclusion_smul
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
Lean source · statement
theorem fixedAlgebraInclusion_smul
    (a : A) (c : fixedAlgebraNative A B G N) :
    (fixedAlgebraInclusion A B G N).toFun (a • c) =
      a • (fixedAlgebraInclusion A B G N).toFun c
def

fixedAlgebraElement

L86 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraElement
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
Lean source · statement
def fixedAlgebraElement (x : B) (hx : ∀ n ∈ N, n • x = x) :
    fixedAlgebraNative A B G N
abbrev

fixedAlgebraQuotientAction

L92 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraQuotientAction
Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
variable [N.Normal]
Lean source · statement
abbrev fixedAlgebraQuotientAction :
    MulSemiringAction (G ⧸ N) (fixedAlgebraNative A B G N)
theorem

fixedAlgebraInclusion_quotient_smul

L98 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraInclusion_quotient_smul
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
variable [N.Normal]
attribute [local instance] fixedAlgebraQuotientAction
Lean source · statement
theorem fixedAlgebraInclusion_quotient_smul
    (g : G) (c : fixedAlgebraNative A B G N) :
    (fixedAlgebraInclusion A B G N).toFun ((QuotientGroup.mk g : G ⧸ N) • c) =
      g • (fixedAlgebraInclusion A B G N).toFun c
theorem

fixedAlgebraQuotient_smulCommClass

L103 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraQuotient_smulCommClass
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
variable [N.Normal]
attribute [local instance] fixedAlgebraQuotientAction
Lean source · statement
theorem fixedAlgebraQuotient_smulCommClass :
    SMulCommClass (G ⧸ N) A (fixedAlgebraNative A B G N)
theorem

fixedAlgebraQuotient_isInvariant

L113 ↗
EtaleFundamentalGroups.Inertia.fixedAlgebraQuotient_isInvariant
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
variable [N.Normal]
attribute [local instance] fixedAlgebraQuotientAction
Lean source · statement
theorem fixedAlgebraQuotient_isInvariant [Algebra.IsInvariant A B G] :
    Algebra.IsInvariant A (fixedAlgebraNative A B G N) (G ⧸ N)
def

fixedResidueCoefficient

L128 ↗
EtaleFundamentalGroups.Inertia.fixedResidueCoefficient
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
variable [N.Normal]
attribute [local instance] fixedAlgebraQuotientAction
Lean source · statement
def fixedResidueCoefficient (q : Ideal B) :
    fixedAlgebraNative A B G N →+* B ⧸ q
theorem

fixedResidueCoefficient_comp_base

L133 ↗
EtaleFundamentalGroups.Inertia.fixedResidueCoefficient_comp_base
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
variable [N.Normal]
attribute [local instance] fixedAlgebraQuotientAction
omit [N.Normal] in
Lean source · statement
theorem fixedResidueCoefficient_comp_base (q : Ideal B) :
    (fixedResidueCoefficient A B G N q).comp
        (algebraMap A (fixedAlgebraNative A B G N)) =
      (Ideal.Quotient.mk q).comp (algebraMap A B)
theorem

fixedResidueCoefficient_quotient_smul

L142 ↗
EtaleFundamentalGroups.Inertia.fixedResidueCoefficient_quotient_smul
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
variable [N.Normal]
attribute [local instance] fixedAlgebraQuotientAction
Lean source · statement
theorem fixedResidueCoefficient_quotient_smul
    (q : Ideal B) (g : G) (c : fixedAlgebraNative A B G N) :
    (fixedResidueCoefficient A B G N q).toFun ((QuotientGroup.mk g : G ⧸ N) • c) =
      (Ideal.Quotient.mk q).toFun (g • (fixedAlgebraInclusion A B G N).toFun c)
theorem

fixedResidueCoefficient_element

L150 ↗
EtaleFundamentalGroups.Inertia.fixedResidueCoefficient_element
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
variable [N.Normal]
attribute [local instance] fixedAlgebraQuotientAction
omit [N.Normal] in
Lean source · statement
theorem fixedResidueCoefficient_element
    (q : Ideal B) (x : B) (hx : ∀ n ∈ N, n • x = x) :
    (fixedResidueCoefficient A B G N q).toFun (fixedAlgebraElement A B G N x hx) =
      (Ideal.Quotient.mk q).toFun x
theorem

exists_residue_lift_on_fixed_elements

L157 ↗
EtaleFundamentalGroups.Inertia.exists_residue_lift_on_fixed_elements
Documentation

A finite quotient of an invariant action supplies one original group element whose residue equations hold on every N-fixed original element.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (B : Type v) (G : Type w)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (N : Subgroup G)
variable [N.Normal]
attribute [local instance] fixedAlgebraQuotientAction
Lean source · statement
theorem exists_residue_lift_on_fixed_elements
    [Finite (G ⧸ N)] [Algebra.IsInvariant A B G]
    (q : Ideal B) [q.IsPrime] (φ : (B ⧸ q) ≃+* (B ⧸ q))
    (hφ : φ.toRingHom.comp ((Ideal.Quotient.mk q).comp (algebraMap A B)) =
      (Ideal.Quotient.mk q).comp (algebraMap A B)) :
    ∃ g : G, ∀ x : B, (∀ n ∈ N, n • x = x) →
      (Ideal.Quotient.mk q).toFun (g • x) =
        φ.toRingHom.toFun ((Ideal.Quotient.mk q).toFun x)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.