def Lecture6.yonedaFullyFaithful (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.yoneda.FullyFaithful

The Yoneda embedding C → [Cᵒᵖ, Type] is fully faithful, the categorical input behind functor-of-points reasoning in ramification arguments.

def Lecture6.yonedaLemmaEquiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) : (CategoryTheory.yoneda.obj X ⟶ F) ≃ F.obj (Opposite.op X)

The Yoneda lemma: natural transformations Hom(−, X) → F correspond bijectively to elements of F(X).

def Lecture6.ramificationIdeal (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.Finite A B] [Module.Free A B] : Ideal A

The principal ramification ideal (disc(A → B)) of A, generated by the discriminant of a chosen basis of the free finite extension B / A.

theorem Lecture6.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 (PrimeSpectrum.zeroLocus ↑(ramificationIdeal A B))

The ramification locus is closed in Spec A, being the zero locus of the discriminant ideal (Lec 6 variant of Prop 7).

theorem Lecture6.ramificationLocus_ne_univ (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] (hsep : Algebra.discr A ⇑(Module.Free.chooseBasis A B) ≠ 0) : PrimeSpectrum.zeroLocus ↑(ramificationIdeal A B) ≠ Set.univ

If the discriminant is nonzero, the ramification locus is a proper closed subset of Spec A.

theorem Lecture6.discr_ne_zero_of_separable (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Module.Finite K L] [Algebra.IsSeparable K L] : Algebra.discr K ⇑(Module.Free.chooseBasis K L) ≠ 0

For a finite separable extension of fields K → L, the discriminant of any chosen basis is nonzero.

noncomputable def Lecture6.dominantMorphismDegree (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] : ℕ

The degree of a dominant morphism of irreducible curves: the dimension of the function-field extension K(B) / K(A).