Module

IntegralClosureAutomorphismRestriction.lean

Nyll.SchemeTheory.Normalization.IntegralClosureAutomorphismRestriction

1 declaration indexed from sourceView source ↗

Module documentation

Restriction of automorphisms to integral closures

Bundles restriction of algebra automorphisms to the integral closure as a group homomorphism.

Imports2

Mathlib.Algebra.Algebra.Equiv
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Imported by3

def

integralClosureAutHom

L25 ↗

SchemeTheory.integralClosureAutHom

Documentation

Restrict algebra automorphisms to the actual integral closure.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
universe u v
variable (R : Type u) (B : Type v) [CommRing R] [CommRing B] [Algebra R B]

Lean source · full declaration

def integralClosureAutHom :
    (B ≃ₐ[R] B) →* (integralClosure R B ≃ₐ[R] integralClosure R B) where
  toFun σ := σ.mapIntegralClosure
  map_one' := by
    apply AlgEquiv.ext
    intro b
    apply Subtype.ext
    rfl
  map_mul' σ τ := by
    apply AlgEquiv.ext
    intro b
    apply Subtype.ext
    rfl

Module documentation

Restriction of automorphisms to integral closures

Declarations

integralClosureAutHom