def Proposition7.ramificationLocus (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.Finite A B] [Module.Free A B] : Set (PrimeSpectrum A)

The ramification locus of A → B (with B a free finite A-module) is the zero locus of the discriminant; the closed set where the cover degenerates.

theorem Proposition7.ramificationLocus_isClosed (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.Finite A B] [Module.Free A B] : IsClosed (ramificationLocus A B)

Prop 7 (Lec 6): the ramification locus is closed in Spec A, being the zero locus of a single discriminant element.

theorem Proposition7.ramificationLocus_ne_univ_of_discr_ne_zero (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [CommRing B] [Algebra A B] [Module.Finite A B] [Module.Free A B] (hd : Algebra.discr A ⇑(Module.Free.chooseBasis A B) ≠ 0) : ramificationLocus A B ≠ Set.univ

If the discriminant is nonzero, the ramification locus is a proper closed subset (not all of Spec A); this rules out total degeneration.

theorem Proposition7.discr_ne_zero_of_separable_functionField (A : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [IsDomain B] [Field L] [Algebra B L] [IsFractionRing B L] [Algebra A B] [Module.Finite A B] [Module.Free A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsLocalization (Algebra.algebraMapSubmonoid B (nonZeroDivisors A)) L] [Algebra.IsSeparable K L] [Module.Finite K L] : Algebra.discr A ⇑(Module.Free.chooseBasis A B) ≠ 0

If the function-field extension K → L is separable and finite, the discriminant of the integral extension A → B is nonzero.

theorem Proposition7.ramificationLocus_ne_univ_of_separable (A : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [CommRing B] [IsDomain B] [Field L] [Algebra B L] [IsFractionRing B L] [Algebra A B] [Module.Finite A B] [Module.Free A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsLocalization (Algebra.algebraMapSubmonoid B (nonZeroDivisors A)) L] [Algebra.IsSeparable K L] [Module.Finite K L] : ramificationLocus A B ≠ Set.univ

Combined version of Prop 7: under a separable finite function-field extension, the ramification locus is a proper closed subset of Spec A.