NYLL
Module

NativeAlgebraResidueLocalization.lean

Nyll.SchemeTheory.RingTheory.Ramification.NativeAlgebraResidueLocalization
3 declarations indexed from sourceView source ↗

Module documentation

Algebra residue morphisms and localization

Identifies the algebra residue morphism with the quotient automorphism of its coefficient action. The canonical maximal-quotient equivalence then relates it to the localization residue map.

Imports9
Imported by2

Declarations

theorem

nativeAlgebraResidueMorphism_eq_quotientEquiv

L38 ↗
EtaleFundamentalGroups.Inertia.nativeAlgebraResidueMorphism_eq_quotientEquiv
Documentation

The same native algebra residue morphism induces the quotient of its actual coefficient automorphism. Its defining coefficient equation is retained.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
open scoped Pointwise
universe u v
Lean source · statement
theorem nativeAlgebraResidueMorphism_eq_quotientEquiv
    {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)
    (d : nativeResidueStabilizer R G Q) :
    nativeAlgebraResidueAutomorphismRingEquiv R Q
        ((nativeAlgebraResidueMorphism R G Q hbase).hom'.toFun d) =
      Ideal.quotientEquiv Q Q (stabilizerCoefficientRingEquiv R G Q d)
        ((congrArg (Ideal.map (stabilizerCoefficientRingEquiv R G Q d).toRingHom)
          (stabilizerCoefficientRingEquiv_comap_eq R G Q d)).trans
          (Ideal.map_comap_eq_self_of_equiv (stabilizerCoefficientRingEquiv R G Q d) Q)).symm
theorem

nativeAlgebraResidueMorphism_localization_square

L72 ↗
EtaleFundamentalGroups.Inertia.nativeAlgebraResidueMorphism_localization_square
Documentation

The same native algebra residue morphism agrees with the actual localization residue map through the fixed maximal-quotient equivalence.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
open scoped Pointwise
universe u v
Lean source · statement
theorem nativeAlgebraResidueMorphism_localization_square
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (G : Type v) [Group G] [MulSemiringAction G R]
    (Q : Ideal R) [Q.IsMaximal]
    (hbase : ∀ g : G, (MulSemiringAction.toRingHom G R g).comp
      (commAlgCoefficientMap R) = commAlgCoefficientMap R)
    (d : nativeResidueStabilizer R G Q) (x : R ⧸ Q) :
    (IsLocalRing.ResidueField.mapEquiv
        (stabilizerLocalizationRingEquiv R G Q d)).toRingHom.toFun
        ((maximalQuotientResidueEquiv Q).toRingHom.toFun x) =
      (maximalQuotientResidueEquiv Q).toRingHom.toFun
        ((nativeAlgebraResidueAutomorphismRingEquiv R Q
          ((nativeAlgebraResidueMorphism R G Q hbase).hom'.toFun d)).toRingHom.toFun x)
theorem

nativeAlgebraResidueMorphism_localization_ringHom

L96 ↗
EtaleFundamentalGroups.Inertia.nativeAlgebraResidueMorphism_localization_ringHom
Documentation

The standard local residue action is the fixed canonical conjugate of the SAME native algebra residue morphism.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
open scoped Pointwise
universe u v
Lean source · statement
theorem nativeAlgebraResidueMorphism_localization_ringHom
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (G : Type v) [Group G] [MulSemiringAction G R]
    (Q : Ideal R) [Q.IsMaximal]
    (hbase : ∀ g : G, (MulSemiringAction.toRingHom G R g).comp
      (commAlgCoefficientMap R) = commAlgCoefficientMap R)
    (d : nativeResidueStabilizer R G Q) :
    MulSemiringAction.toRingHom (MulAction.stabilizer G Q) Q.ResidueField d =
      ((maximalQuotientResidueEquiv Q).toRingHom.comp
        (nativeAlgebraResidueAutomorphismRingEquiv R Q
          ((nativeAlgebraResidueMorphism R G Q hbase).hom'.toFun d)).toRingHom).comp
        (maximalQuotientResidueEquiv Q).symm.toRingHom

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