NYLL
Module

CommAlgStabilizerResidueMorphism.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgStabilizerResidueMorphism
2 declarations indexed from sourceView source ↗

Module documentation

Residue morphisms for intrinsic stabilizers

Proves coefficient preservation by intrinsic algebra automorphisms and constructs the resulting native quotient-residue morphism.

Imports5
Imported by4

Declarations

theorem

commAlgAutomorphism_comp_coefficient

L29 ↗
EtaleFundamentalGroups.Inertia.commAlgAutomorphism_comp_coefficient
Documentation

The intrinsic algebra automorphisms preserve the stored coefficient map.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
Lean source · statement
theorem commAlgAutomorphism_comp_coefficient
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (σ : B ≃ₐ[A] B) :
    (MulSemiringAction.toRingHom (B ≃ₐ[A] B) B σ).comp
        (commAlgCoefficientMap B) = commAlgCoefficientMap B
def

commAlgStabilizerResidueMorphism

L38 ↗
EtaleFundamentalGroups.Inertia.commAlgStabilizerResidueMorphism
Documentation

The same native quotient-residue morphism for the actual intrinsic normalization automorphisms, with coefficient preservation proved above.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
Lean source · statement
def commAlgStabilizerResidueMorphism
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B) :
    GrpCat.Hom (nativeResidueStabilizer B (B ≃ₐ[A] B) Q)
      (nativeAlgebraResidueAutomorphisms B Q)

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