Restriction of various maps between fields to integrally closed subrings. #

In this file, we assume A is an integrally closed domain; K is the fraction ring of A; L is a finite (separable) extension of K; B is the integral closure of A in L. We call this the AKLB setup.

Main definition #

galRestrict: The restriction Aut(L/K) → Aut(B/A) as an MulEquiv in an AKLB setup.
Algebra.intTrace: The trace map of a finite extension of integrally closed domains B/A is defined to be the restriction of the trace map of Frac(B)/Frac(A).
Algebra.intNorm: The norm map of a finite extension of integrally closed domains B/A is defined to be the restriction of the norm map of Frac(B)/Frac(A).

source

noncomputable def galLift (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] (σ : B →ₐ[A] B) :

L →ₐ[K] L

The lift End(B/A) → End(L/K) in an ALKB setup. This is inverse to the restriction. See galRestrictHom.

Equations

galLift A K L B σ = { toRingHom := IsLocalization.lift ⋯, commutes' := ⋯ }

Instances For

source

noncomputable def galRestrictHom (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] :

(L →ₐ[K] L) ≃* (B →ₐ[A] B)

The restriction End(L/K) → End(B/A) in an AKLB setup. Also see galRestrict for the AlgEquiv version.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem algebraMap_galRestrictHom_apply (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] (σ : L →ₐ[K] L) (x : B) :

(algebraMap B L) (((galRestrictHom A K L B) σ) x) = σ ((algebraMap B L) x)

source

@[simp]

theorem galRestrictHom_symm_algebraMap_apply (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] (σ : B →ₐ[A] B) (x : B) :

((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)

source

noncomputable def galRestrict (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] :

(L ≃ₐ[K] L) ≃* B ≃ₐ[A] B

The restriction Aut(L/K) → Aut(B/A) in an AKLB setup.

Equations

galRestrict A K L B = (AlgEquiv.algHomUnitsEquiv K L).symm.trans ((Units.mapEquiv (galRestrictHom A K L B)).trans (AlgEquiv.algHomUnitsEquiv A B))

Instances For

source

theorem coe_galRestrict_apply (A : Type u_1) {K : Type u_2} {L : Type u_3} (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] (σ : L ≃ₐ[K] L) :

↑((galRestrict A K L B) σ) = (galRestrictHom A K L B) ↑σ

source

theorem galRestrict_apply (A : Type u_1) {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] (σ : L ≃ₐ[K] L) (x : B) :

((galRestrict A K L B) σ) x = ((galRestrictHom A K L B) ↑σ) x

source

theorem algebraMap_galRestrict_apply (A : Type u_1) {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] (σ : L ≃ₐ[K] L) (x : B) :

(algebraMap B L) (((galRestrict A K L B) σ) x) = σ ((algebraMap B L) x)

source

theorem prod_galRestrict_eq_norm (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsGalois K L] [IsIntegrallyClosed A] (x : B) :

∏ σ : L ≃ₐ[K] L, ((galRestrict A K L B) σ) x = (algebraMap A B) (IsIntegralClosure.mk' A ((Algebra.norm K) ((algebraMap B L) x)) ⋯)

source

@[instance 900]

noncomputable instance instFintypeAlgEquivOfIsDomainOfIsIntegrallyClosedOfFiniteOfNoZeroSMulDivisors (A : Type u_1) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] :

Fintype (B ≃ₐ[A] B)

Equations

One or more equations did not get rendered due to their size.

source

noncomputable def Algebra.intTraceAux (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsIntegrallyClosed A] :

B →ₗ[A] A

The restriction of the trace on L/K restricted onto B/A in an AKLB setup. See Algebra.intTrace instead.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Algebra.map_intTraceAux {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsIntegrallyClosed A] (x : B) :

(algebraMap A K) ((Algebra.intTraceAux A K L B) x) = (Algebra.trace K L) ((algebraMap B L) x)

source

noncomputable def Algebra.intTrace (A : Type u_1) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] :

B →ₗ[A] A

The trace of a finite extension of integrally closed domains B/A is the restriction of the trace on Frac(B)/Frac(A) onto B/A. See Algebra.algebraMap_intTrace.

Equations

Algebra.intTrace A B = Algebra.intTraceAux A (FractionRing A) (FractionRing B) B

Instances For

source

theorem Algebra.algebraMap_intTrace {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] (x : B) :

(algebraMap A K) ((Algebra.intTrace A B) x) = (Algebra.trace K L) ((algebraMap B L) x)

source

theorem Algebra.algebraMap_intTrace_fractionRing {A : Type u_1} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] (x : B) :

(algebraMap A (FractionRing A)) ((Algebra.intTrace A B) x) = (Algebra.trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)

source

theorem Algebra.intTrace_eq_trace (A : Type u_1) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] [Module.Free A B] :

Algebra.intTrace A B = Algebra.trace A B

source

theorem Algebra.intTrace_eq_of_isLocalization (A : Type u_1) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] {Aₘ : Type u_5} {Bₘ : Type u_6} [CommRing Aₘ] [CommRing Bₘ] [Algebra Aₘ Bₘ] [Algebra A Aₘ] [Algebra B Bₘ] [Algebra A Bₘ] [IsScalarTower A Aₘ Bₘ] [IsScalarTower A B Bₘ] (M : Submonoid A) [IsLocalization M Aₘ] [IsLocalization (Algebra.algebraMapSubmonoid B M) Bₘ] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] [IsDomain Aₘ] [IsIntegrallyClosed Aₘ] [IsDomain Bₘ] [IsIntegrallyClosed Bₘ] [NoZeroSMulDivisors Aₘ Bₘ] [Module.Finite Aₘ Bₘ] (x : B) :

(algebraMap A Aₘ) ((Algebra.intTrace A B) x) = (Algebra.intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)

source

noncomputable def Algebra.intNormAux (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsIntegrallyClosed A] [Algebra.IsSeparable K L] :

B →* A

The restriction of the norm on L/K restricted onto B/A in an AKLB setup. See Algebra.intNorm instead.

Equations

Algebra.intNormAux A K L B = { toFun := fun (s : B) => IsIntegralClosure.mk' A ((Algebra.norm K) ((algebraMap B L) s)) ⋯, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

theorem Algebra.map_intNormAux {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsIntegrallyClosed A] [Algebra.IsSeparable K L] (x : B) :

(algebraMap A K) ((Algebra.intNormAux A K L B) x) = (Algebra.norm K) ((algebraMap B L) x)

source

noncomputable def Algebra.intNorm (A : Type u_1) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] [IsIntegrallyClosed A] [IsDomain A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] :

B →* A

The norm of a finite extension of integrally closed domains B/A is the restriction of the norm on Frac(B)/Frac(A) onto B/A. See Algebra.algebraMap_intNorm.

Equations