Containment of a component’s conormal closure in the ambient characteristic variety.

theorem Stafford38.Geometry.GeneralComponentConormalContainment.equationConormalClosure_minimalPrime_subset_zeroLocus {k : Type u} [Field k] [IsAlgClosed k] [CharZero k] {n : ℕ} (J : Ideal (Characteristic.SymbolRing k n)) (hJrad : J.IsRadical) (hhom : Ideal.IsHomogeneous GeneralConormalContainment.orderDecomposition J) (hJpoisson : Characteristic.BaseRelativePoisson.IsBaseRelativePoisson J) (P : Ideal (MvPolynomial (Fin n) k)) (hP : P ∈ (Ideal.comap CoisotropicTranslation.baseLift J).minimalPrimes) : AffineConormalClosure.equationConormalClosure P ⊆ MvPolynomial.zeroLocus k J

theorem Stafford38.Geometry.GeneralComponentConormalContainment.smoothConormalClosure_minimalPrime_subset_zeroLocus {k : Type u} [Field k] [IsAlgClosed k] [CharZero k] {n : ℕ} (J : Ideal (Characteristic.SymbolRing k n)) (hJrad : J.IsRadical) (hhom : Ideal.IsHomogeneous GeneralConormalContainment.orderDecomposition J) (hJpoisson : Characteristic.BaseRelativePoisson.IsBaseRelativePoisson J) (P : Ideal (MvPolynomial (Fin n) k)) (hP : P ∈ (Ideal.comap CoisotropicTranslation.baseLift J).minimalPrimes) : MvPolynomial.zeroLocus k (MvPolynomial.vanishingIdeal k (ConormalPrincipalOpenDensity.restrictedEquationConormalLocus P {y : Fin n → k | SmoothAffineConormal.SmoothAffinePoint P y})) ⊆ MvPolynomial.zeroLocus k J