@[reducible, inline]
abbrev
LocalIntersection.IntersectionQuotient
(k : Type u_1)
[Field k]
(f g : MvPolynomial (Fin 2) k)
:
Type u_1
The quotient ring k[x,y]/(f,g) used to define intersection multiplicities.
Instances For
noncomputable def
LocalIntersection.mulByXOp
(k : Type u_1)
[Field k]
(f g : MvPolynomial (Fin 2) k)
:
Module.End k (IntersectionQuotient k f g)
Multiplication by x as a k-linear endomorphism of the intersection quotient.
Instances For
noncomputable def
LocalIntersection.mulByYOp
(k : Type u_1)
[Field k]
(f g : MvPolynomial (Fin 2) k)
:
Module.End k (IntersectionQuotient k f g)
Multiplication by y as a k-linear endomorphism of the intersection quotient.
Instances For
noncomputable def
LocalIntersection.commonGenEigenspace
(k : Type u_1)
[Field k]
(f g : MvPolynomial (Fin 2) k)
(a b : k)
:
Submodule k (IntersectionQuotient k f g)
The common generalized eigenspace where x acts with generalized eigenvalue a
and y with generalized eigenvalue b.
Instances For
noncomputable def
LocalIntersection.localIntersectionMultiplicity
(k : Type u_1)
[Field k]
(f g : MvPolynomial (Fin 2) k)
(a b : k)
:
The local intersection multiplicity of f and g at the point (a,b) is the
k-dimension of the common generalized eigenspace (Def 13, Lec 5).
Instances For
noncomputable def
LocalIntersection.totalIntersectionNumberMv
(k : Type u_1)
[Field k]
(f g : MvPolynomial (Fin 2) k)
:
The total intersection number of f and g is the k-dimension of the
intersection quotient k[x,y]/(f,g).
Instances For
theorem
LocalIntersection.localIntersectionMultiplicity_eq_finrank
(k : Type u_1)
[Field k]
(f g : MvPolynomial (Fin 2) k)
(a b : k)
:
localIntersectionMultiplicity k f g a b = Module.finrank k ↥((mulByXOp k f g).maxGenEigenspace a ⊓ (mulByYOp k f g).maxGenEigenspace b)
The local intersection multiplicity equals the k-dimension of the common
generalized eigenspace, by definition.