NYLL
Module

RingActionInvariantPreimage.lean

Nyll.SchemeTheory.RingTheory.Ramification.RingActionInvariantPreimage
11 declarations indexed from sourceView source ↗

Module documentation

Actual inertia-fixed preimages in a ring-action restriction

An injective equivariant ring map and the proved full inertia image give the equality between the actual upper-fixed preimage and the actual lower fixed ring. The proof stays in the existing ring-action restriction owner; no field, coefficient algebra, or localization is introduced.

Imports4
Imported by2

Declarations

def

upperInertiaFixedSubring

L28 ↗
SchemeTheory.RingActionRestriction.upperInertiaFixedSubring
Documentation

The actual upper inertia-fixed subring for the prescribed action.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
def upperInertiaFixedSubring (D : RingActionRestriction.{u, v, w, x})
    (q : Ideal D.upperRing.carrier) : Subring D.upperRing.carrier
def

lowerInertiaFixedSubring

L34 ↗
SchemeTheory.RingActionRestriction.lowerInertiaFixedSubring
Documentation

The actual lower inertia-fixed subring for the prescribed action.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
def lowerInertiaFixedSubring (D : RingActionRestriction.{u, v, w, x})
    (p : Ideal D.lowerRing.carrier) : Subring D.lowerRing.carrier
def

inertiaFixedPreimageSubring

L40 ↗
SchemeTheory.RingActionRestriction.inertiaFixedPreimageSubring
Documentation

The literal preimage of upper inertia invariants under the given ring map.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
def inertiaFixedPreimageSubring (D : RingActionRestriction.{u, v, w, x})
    (q : Ideal D.upperRing.carrier) : Subring D.lowerRing.carrier
theorem

inertiaFixedPreimageSubring_eq

L46 ↗
SchemeTheory.RingActionRestriction.inertiaFixedPreimageSubring_eq
Documentation

The existing equivariant square and the full inertia image prove the actual fixed-ring comparison. No comparison is part of the data owner.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
theorem inertiaFixedPreimageSubring_eq (D : RingActionRestriction.{u, v, w, x})
    (p : Ideal D.lowerRing.carrier) (q : Ideal D.upperRing.carrier)
    (hinj : Function.Injective D.ringMap.toFun) (hequiv : D.IsEquivariant)
    (himage : (D.upperInertia q).map D.groupMap = D.lowerInertia p) :
    D.inertiaFixedPreimageSubring q = D.lowerInertiaFixedSubring p
def

upperInertiaFixedRing

L83 ↗
SchemeTheory.RingActionRestriction.upperInertiaFixedRing
Documentation

The native upper inertia-fixed ring object.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
def upperInertiaFixedRing (D : RingActionRestriction.{u, v, w, x})
    (q : Ideal D.upperRing.carrier) : CommRingCat.{v}
def

lowerInertiaFixedRing

L88 ↗
SchemeTheory.RingActionRestriction.lowerInertiaFixedRing
Documentation

The native lower inertia-fixed ring object.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
def lowerInertiaFixedRing (D : RingActionRestriction.{u, v, w, x})
    (p : Ideal D.lowerRing.carrier) : CommRingCat.{u}
def

inertiaFixedPreimageRing

L93 ↗
SchemeTheory.RingActionRestriction.inertiaFixedPreimageRing
Documentation

The native actual preimage ring object.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
def inertiaFixedPreimageRing (D : RingActionRestriction.{u, v, w, x})
    (q : Ideal D.upperRing.carrier) : CommRingCat.{u}
def

inertiaFixedPreimageInclusion

L98 ↗
SchemeTheory.RingActionRestriction.inertiaFixedPreimageInclusion
Documentation

The literal preimage inclusion into the upper fixed ring.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
def inertiaFixedPreimageInclusion (D : RingActionRestriction.{u, v, w, x})
    (q : Ideal D.upperRing.carrier) :
    (D.inertiaFixedPreimageRing q).carrier →+* (D.upperInertiaFixedRing q).carrier
theorem

inertiaFixedPreimageInclusion_comp_subtype

L105 ↗
SchemeTheory.RingActionRestriction.inertiaFixedPreimageInclusion_comp_subtype
Documentation

The preimage inclusion retains the actual original coefficient map.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
theorem inertiaFixedPreimageInclusion_comp_subtype
    (D : RingActionRestriction.{u, v, w, x}) (q : Ideal D.upperRing.carrier) :
    (D.upperInertiaFixedSubring q).subtype.comp (D.inertiaFixedPreimageInclusion q) =
      D.ringMap.comp (D.inertiaFixedPreimageSubring q).subtype
def

inertiaFixedPreimageEquiv

L113 ↗
SchemeTheory.RingActionRestriction.inertiaFixedPreimageEquiv
Documentation

The proved actual comparison, with no new coefficient action.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
def inertiaFixedPreimageEquiv (D : RingActionRestriction.{u, v, w, x})
    (p : Ideal D.lowerRing.carrier) (q : Ideal D.upperRing.carrier)
    (hinj : Function.Injective D.ringMap.toFun) (hequiv : D.IsEquivariant)
    (himage : (D.upperInertia q).map D.groupMap = D.lowerInertia p) :
    (D.inertiaFixedPreimageRing q).carrier ≃+* (D.lowerInertiaFixedRing p).carrier
theorem

inertiaFixedPreimageEquiv_comp_subtype

L121 ↗
SchemeTheory.RingActionRestriction.inertiaFixedPreimageEquiv_comp_subtype
Documentation

The comparison is exactly the identity on lower normalization elements.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory.RingActionRestriction
universe u v w x
Lean source · statement
theorem inertiaFixedPreimageEquiv_comp_subtype
    (D : RingActionRestriction.{u, v, w, x})
    (p : Ideal D.lowerRing.carrier) (q : Ideal D.upperRing.carrier)
    (hinj : Function.Injective D.ringMap.toFun) (hequiv : D.IsEquivariant)
    (himage : (D.upperInertia q).map D.groupMap = D.lowerInertia p) :
    (D.lowerInertiaFixedSubring p).subtype.comp
        (D.inertiaFixedPreimageEquiv p q hinj hequiv himage).toRingHom =
      (D.inertiaFixedPreimageSubring q).subtype

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