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 galRestrict' (A : Type u_1) {K : Type u_2} {L : Type u_3} {L₂ : Type u_4} (B : Type u_6) (B₂ : Type u_7) [CommRing A] [CommRing B] [CommRing B₂] [Algebra A B] [Algebra A B₂] [Field K] [Field L] [Field L₂] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra K L₂] [Algebra A L₂] [IsScalarTower A K L₂] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra B₂ L₂] [IsScalarTower A B₂ L₂] [IsIntegralClosure B₂ A L₂] (f : L →ₐ[K] L₂) : B →ₐ[A] B₂

A generalization of galRestrictHom beyond endomorphisms.

Equations

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

@[simp]

theorem algebraMap_galRestrict'_apply (A : Type u_1) {K : Type u_2} {L : Type u_3} {L₂ : Type u_4} (B : Type u_6) (B₂ : Type u_7) [CommRing A] [CommRing B] [CommRing B₂] [Algebra A B] [Algebra A B₂] [Field K] [Field L] [Field L₂] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra K L₂] [Algebra A L₂] [IsScalarTower A K L₂] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra B₂ L₂] [IsScalarTower A B₂ L₂] [IsIntegralClosure B₂ A L₂] (σ : L →ₐ[K] L₂) (x : B) : (algebraMap B₂ L₂) ((galRestrict' A B B₂ σ) x) = σ ((algebraMap B L) x)

theorem galRestrict'_comp (A : Type u_1) {K : Type u_2} {L : Type u_3} {L₂ : Type u_4} {L₃ : Type u_5} (B : Type u_6) (B₂ : Type u_7) (B₃ : Type u_8) [CommRing A] [CommRing B] [CommRing B₂] [CommRing B₃] [Algebra A B] [Algebra A B₂] [Algebra A B₃] [Field K] [Field L] [Field L₂] [Field L₃] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra K L₂] [Algebra A L₂] [IsScalarTower A K L₂] [Algebra K L₃] [Algebra A L₃] [IsScalarTower A K L₃] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra B₂ L₂] [IsScalarTower A B₂ L₂] [IsIntegralClosure B₂ A L₂] [Algebra B₃ L₃] [IsScalarTower A B₃ L₃] [IsIntegralClosure B₃ A L₃] (σ : L →ₐ[K] L₂) (σ' : L₂ →ₐ[K] L₃) : galRestrict' A B B₃ (σ'.comp σ) = (galRestrict' A B₂ B₃ σ').comp (galRestrict' A B B₂ σ)

noncomputable def galLift {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [CommRing A] [CommRing B] [CommRing B₂] [Algebra A B] [Algebra A B₂] [Field K] [Field L] [Field L₂] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra K L₂] [Algebra A L₂] [IsScalarTower A K L₂] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra B₂ L₂] [IsScalarTower A B₂ L₂] [Algebra.IsAlgebraic K L] (σ : B →ₐ[A] B₂) : L →ₐ[K] L₂

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

Equations

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

@[simp]

theorem galLift_algebraMap_apply {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [CommRing A] [CommRing B] [CommRing B₂] [Algebra A B] [Algebra A B₂] [Field K] [Field L] [Field L₂] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra K L₂] [Algebra A L₂] [IsScalarTower A K L₂] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra B₂ L₂] [IsScalarTower A B₂ L₂] [Algebra.IsAlgebraic K L] (σ : B →ₐ[A] B₂) (x : B) : (galLift K L L₂ σ) ((algebraMap B L) x) = (algebraMap B₂ L₂) (σ x)

theorem galLift_comp {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) (L₃ : Type u_5) {B : Type u_6} {B₂ : Type u_7} {B₃ : Type u_8} [CommRing A] [CommRing B] [CommRing B₂] [CommRing B₃] [Algebra A B] [Algebra A B₂] [Algebra A B₃] [Field K] [Field L] [Field L₂] [Field L₃] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra K L₂] [Algebra A L₂] [IsScalarTower A K L₂] [Algebra K L₃] [Algebra A L₃] [IsScalarTower A K L₃] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra B₂ L₂] [IsScalarTower A B₂ L₂] [IsIntegralClosure B₂ A L₂] [Algebra B₃ L₃] [IsScalarTower A B₃ L₃] [Algebra.IsAlgebraic K L] [Algebra.IsAlgebraic K L₂] (σ : B →ₐ[A] B₂) (σ' : B₂ →ₐ[A] B₃) : galLift K L L₃ (σ'.comp σ) = (galLift K L₂ L₃ σ').comp (galLift K L L₂ σ)

@[simp]

theorem galLift_galRestrict' {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [CommRing A] [CommRing B] [CommRing B₂] [Algebra A B] [Algebra A B₂] [Field K] [Field L] [Field L₂] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra K L₂] [Algebra A L₂] [IsScalarTower A K L₂] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra B₂ L₂] [IsScalarTower A B₂ L₂] [IsIntegralClosure B₂ A L₂] [Algebra.IsAlgebraic K L] (σ : L →ₐ[K] L₂) : galLift K L L₂ (galRestrict' A B B₂ σ) = σ

@[simp]

theorem galRestrict'_galLift {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [CommRing A] [CommRing B] [CommRing B₂] [Algebra A B] [Algebra A B₂] [Field K] [Field L] [Field L₂] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra K L₂] [Algebra A L₂] [IsScalarTower A K L₂] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra B₂ L₂] [IsScalarTower A B₂ L₂] [IsIntegralClosure B₂ A L₂] [Algebra.IsAlgebraic K L] (σ : B →ₐ[A] B₂) : galRestrict' A B B₂ (galLift K L L₂ σ) = σ

noncomputable def galRestrictHom (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic 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

• galRestrictHom A K L B = { toFun := fun (f : L →ₐ[K] L) => galRestrict' A B B f, invFun := galLift K L L, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

theorem galRestrictHom_apply (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic K L] (f : L →ₐ[K] L) : (galRestrictHom A K L B) f = galRestrict' A B B f

theorem galRestrictHom_symm_apply (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic K L] (σ : B →ₐ[A] B) : (galRestrictHom A K L B).symm σ = galLift K L L σ

@[simp]

theorem algebraMap_galRestrictHom_apply (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic 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_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic 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_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic 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_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic 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_6} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic 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_6} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic 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_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B 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)) ⋯)

@[instance 900]

noncomputable instance instFintypeAlgEquivOfIsDomainOfIsIntegrallyClosedOfFiniteOfNoZeroSMulDivisors (A : Type u_1) (B : Type u_6) [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_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B 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_6} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsIntegrallyClosed A] (x : B) : (algebraMap A K) ((intTraceAux A K L B) x) = (trace K L) ((algebraMap B L) x)

noncomputable def Algebra.intTrace (A : Type u_1) (B : Type u_6) [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_6} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B 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) ((intTrace A B) x) = (trace K L) ((algebraMap B L) x)

theorem Algebra.algebraMap_intTrace_fractionRing {A : Type u_1} {B : Type u_6} [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)) ((intTrace A B) x) = (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)

theorem Algebra.intTrace_eq_trace (A : Type u_1) (B : Type u_6) [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] : intTrace A B = trace A B

theorem Algebra.intTrace_eq_of_isLocalization (A : Type u_1) (B : Type u_6) [CommRing A] [CommRing B] [Algebra A B] {Aₘ : Type u_9} {Bₘ : Type u_10} [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 (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ₘ) ((intTrace A B) x) = (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_6) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B 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' := ⋯ }

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

noncomputable def Algebra.intNorm (A : Type u_1) (B : Type u_6) [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

• 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_6} [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L] [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsIntegrallyClosed A] [IsDomain A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (x : B) : (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

@[simp]

theorem Algebra.algebraMap_intNorm_fractionRing {A : Type u_1} {B : Type u_6} [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)] (x : B) : (algebraMap A (FractionRing A)) ((intNorm A B) x) = (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x)

theorem Algebra.intNorm_intNorm (A : Type u_1) (B : Type u_6) [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)] {C : Type u_9} [CommRing C] [IsDomain C] [IsIntegrallyClosed C] [Algebra A C] [Algebra B C] [IsScalarTower A B C] [Module.Finite A C] [Module.Finite B C] [NoZeroSMulDivisors A C] [NoZeroSMulDivisors B C] [Algebra.IsSeparable (FractionRing A) (FractionRing C)] [Algebra.IsSeparable (FractionRing B) (FractionRing C)] (x : C) : (intNorm A B) ((intNorm B C) x) = (intNorm A C) x

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

@[simp]

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

@[simp]

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

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

theorem Algebra.intNorm_eq_of_isLocalization {A : Type u_1} {B : Type u_6} [CommRing A] [CommRing B] [Algebra A B] {Aₘ : Type u_9} {Bₘ : Type u_10} [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 (algebraMapSubmonoid B M) Bₘ] [IsIntegrallyClosed A] [IsDomain A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [IsDomain Aₘ] [IsIntegrallyClosed Aₘ] [IsDomain Bₘ] [IsIntegrallyClosed Bₘ] [NoZeroSMulDivisors Aₘ Bₘ] [Module.Finite Aₘ Bₘ] [Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)] (x : B) : (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

theorem Algebra.algebraMap_intNorm_of_isGalois (A : Type u_1) (B : Type u_6) [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) ((intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x

theorem Algebra.dvd_algebraMap_intNorm_self (A : Type u_1) (B : Type u_6) [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsIntegrallyClosed A] [IsDomain B] [IsIntegrallyClosed B] [Module.Finite A B] [NoZeroSMulDivisors A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] (x : B) : x ∣ (algebraMap A B) ((intNorm A B) x)