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).

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 σ = let __src := IsLocalization.lift ⋯; { toRingHom := __src, commutes' := ⋯ }

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.

@[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)

@[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)

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))

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) ↑σ

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

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)

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) : (Finset.univ.prod fun (σ : L ≃ₐ[K] L) => ((galRestrict A K L B) σ) x) = (algebraMap A B) (IsIntegralClosure.mk' A ((Algebra.norm K) ((algebraMap B L) x)) ⋯)

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.

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.

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)

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

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)

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)

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

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)

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] [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' := ⋯ }

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] [IsSeparable K L] (x : B) : (algebraMap A K) ((Algebra.intNormAux A K L B) x) = (Algebra.norm K) ((algebraMap B L) x)

noncomputable def Algebra.intNorm (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] [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

• Algebra.intNorm A B = Algebra.intNormAux A (FractionRing A) (FractionRing B) B

theorem Algebra.algebraMap_intNorm {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] [IsSeparable (FractionRing A) (FractionRing B)] (x : B) : (algebraMap A K) ((Algebra.intNorm A B) x) = (Algebra.norm K) ((algebraMap B L) x)

@[simp]

theorem Algebra.algebraMap_intNorm_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] [IsSeparable (FractionRing A) (FractionRing B)] (x : B) : (algebraMap A (FractionRing A)) ((Algebra.intNorm A B) x) = (Algebra.norm (FractionRing A)) ((algebraMap B (FractionRing B)) x)

theorem Algebra.intNorm_eq_norm (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] [IsSeparable (FractionRing A) (FractionRing B)] [Module.Free A B] : Algebra.intNorm A B = Algebra.norm A

@[simp]

theorem Algebra.intNorm_zero (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] [IsSeparable (FractionRing A) (FractionRing B)] : (Algebra.intNorm A B) 0 = 0

@[simp]

theorem Algebra.intNorm_eq_zero {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] [IsSeparable (FractionRing A) (FractionRing B)] {x : B} : (Algebra.intNorm A B) x = 0 ↔ x = 0

theorem Algebra.intNorm_ne_zero {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] [IsSeparable (FractionRing A) (FractionRing B)] {x : B} : (Algebra.intNorm A B) x ≠ 0 ↔ x ≠ 0

theorem Algebra.intNorm_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] [IsSeparable (FractionRing A) (FractionRing B)] [IsDomain Aₘ] [IsIntegrallyClosed Aₘ] [IsDomain Bₘ] [IsIntegrallyClosed Bₘ] [NoZeroSMulDivisors Aₘ Bₘ] [Module.Finite Aₘ Bₘ] [IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)] (x : B) : (algebraMap A Aₘ) ((Algebra.intNorm A B) x) = (Algebra.intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

theorem Algebra.algebraMap_intNorm_of_isGalois (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] [IsGalois (FractionRing A) (FractionRing B)] {x : B} : (algebraMap A B) ((Algebra.intNorm A B) x) = Finset.univ.prod fun (σ : B ≃ₐ[A] B) => σ x