noncomputable def finite_birational_normal_algEquiv (B : Type u_1) (A : Type u_2) (K : Type u_3) [CommRing B] [IsDomain B] [CommRing A] [Field K] [Algebra B K] [IsFractionRing B K] [Algebra A K] [Algebra B A] [IsScalarTower B A K] [IsIntegrallyClosed B] [IsIntegralClosure A B K] : A ≃ₐ[B] B

If B is an integrally closed domain with fraction field K and A is the integral closure of B in K, then A is algebra-isomorphic to B (so a finite birational map over a normal base is an isomorphism).

theorem finite_birational_normal_algebraMap_bijective (B : Type u_1) (A : Type u_2) (K : Type u_3) [CommRing B] [IsDomain B] [CommRing A] [Field K] [Algebra B K] [IsFractionRing B K] [Algebra A K] [Algebra B A] [IsScalarTower B A K] [IsIntegrallyClosed B] [IsIntegralClosure A B K] : Function.Bijective ⇑(algebraMap B A)

Under the same hypotheses as finite_birational_normal_algEquiv, the structure map B → A is bijective.

noncomputable def normalization_of_normal_is_self (A : Type u_1) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] : ↥(integralClosure A (FractionRing A)) ≃ₐ[A] A

The normalization of an integrally closed domain A (its integral closure in its fraction field) is A itself.

theorem normalization_is_finite_general (k : Type u_1) (A : Type u_2) [Field k] [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] : Module.Finite A ↥(integralClosure A L)

Proposition 28 (finiteness part): For a finitely generated k-algebra domain A with fraction field K and a finite field extension L/K, the integral closure of A in L is finite over A.

theorem normalization_finiteType_general (k : Type u_1) (A : Type u_2) [Field k] [CommRing A] [IsDomain A] [Algebra k A] [Algebra.FiniteType k A] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [Algebra k K] [IsScalarTower k A K] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] [Algebra k L] [IsScalarTower k A L] : Algebra.FiniteType k ↥(integralClosure A L)

Proposition 28 (finite-type part): The integral closure of A in L remains of finite type over the base field k.

theorem normalization_is_normal_general (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] : IsIntegrallyClosed ↥(integralClosure A L)

Proposition 28 (normality part): The integral closure of A in a finite extension L is itself integrally closed.

theorem normalization_map_injective_general (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] : Function.Injective ⇑(algebraMap A ↥(integralClosure A L))

The structure map A → integralClosure A L is injective, so normalization does not collapse the base.