noncomputable def totalDerivativeAt {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin n) k) (P v : Fin n → k) : k

noncomputable def totalDerivativeAtLin {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin n) k) (P : Fin n → k) : (Fin n → k) →ₗ[k] k

noncomputable def tangentSpacePoly {k : Type u_1} [Field k] {n : ℕ} (f : MvPolynomial (Fin n) k) (P : Fin n → k) : Submodule k (Fin n → k)

noncomputable def tangentSpaceIdeal {k : Type u_1} [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) k)) (P : Fin n → k) : Submodule k (Fin n → k)

theorem totalDerivativeAt_add {k : Type u_1} [Field k] {n : ℕ} (f g : MvPolynomial (Fin n) k) (P v : Fin n → k) : totalDerivativeAt (f + g) P v = totalDerivativeAt f P v + totalDerivativeAt g P v

theorem totalDerivativeAt_zero {k : Type u_1} [Field k] {n : ℕ} (P v : Fin n → k) : totalDerivativeAt 0 P v = 0

theorem totalDerivativeAt_mul_of_eval_eq_zero {k : Type u_1} [Field k] {n : ℕ} (r g : MvPolynomial (Fin n) k) (P v : Fin n → k) (hg : (MvPolynomial.eval P) g = 0) : totalDerivativeAt (r * g) P v = (MvPolynomial.eval P) r * totalDerivativeAt g P v

theorem totalDerivativeAt_smul_of_eval_eq_zero {k : Type u_1} [Field k] {n : ℕ} (r g : MvPolynomial (Fin n) k) (P v : Fin n → k) (hg : (MvPolynomial.eval P) g = 0) : totalDerivativeAt (r • g) P v = (MvPolynomial.eval P) r * totalDerivativeAt g P v

theorem tangentSpaceIdeal_eq_iInf_generators {k : Type u_1} [Field k] {n m : ℕ} (f : Fin m → MvPolynomial (Fin n) k) (P : Fin n → k) (hP : ∀ g ∈ Ideal.span (Set.range f), (MvPolynomial.eval P) g = 0) : tangentSpaceIdeal (Ideal.span (Set.range f)) P = ⨅ (i : Fin m), tangentSpacePoly (f i) P

theorem tangentSpace_eq_ker_jacobian {k : Type u_1} [Field k] {n m : ℕ} (f : Fin m → MvPolynomial (Fin n) k) (P : Fin n → k) : ⨅ (i : Fin m), tangentSpacePoly (f i) P = (Matrix.of fun (i : Fin m) (j : Fin n) => (MvPolynomial.eval P) ((MvPolynomial.pderiv j) (f i))).mulVecLin.ker

noncomputable def jointLinearizationMap {k : Type u_1} [Field k] {n m : ℕ} (f : Fin m → MvPolynomial (Fin n) k) (P : Fin n → k) : (Fin n → k) →ₗ[k] Fin m → k

theorem tangentSpace_eq_ker_jointLinearizationMap {k : Type u_1} [Field k] {n m : ℕ} (f : Fin m → MvPolynomial (Fin n) k) (P : Fin n → k) : ⨅ (i : Fin m), tangentSpacePoly (f i) P = (jointLinearizationMap f P).ker

theorem cotangentSpace_dualAnnihilator_eq_range_dualMap {k : Type u_1} [Field k] {n m : ℕ} (f : Fin m → MvPolynomial (Fin n) k) (P : Fin n → k) : (⨅ (i : Fin m), tangentSpacePoly (f i) P).dualAnnihilator = (jointLinearizationMap f P).dualMap.range

noncomputable def TangentSpaces.jacobianMatrix {k : Type u_1} [Field k] (n m : ℕ) (f : Fin m → MvPolynomial (Fin n) k) (P : Fin n → k) : Matrix (Fin m) (Fin n) k

def TangentSpaces.tangentSpace {k : Type u_1} [Field k] {m n : ℕ} (M : Matrix (Fin m) (Fin n) k) : Submodule k (Fin n → k)

def TangentSpaces.cotangentSpaceDual {k : Type u_1} [Field k] {m n : ℕ} (M : Matrix (Fin m) (Fin n) k) : Submodule k (Module.Dual k (Fin n → k))

def TangentSpaces.cotangentSpace {k : Type u_1} [Field k] {m n : ℕ} (M : Matrix (Fin m) (Fin n) k) : Submodule k (Fin m → k)

theorem TangentSpaces.tangent_dim_eq_sub_jacobian_rank {k : Type u_1} [Field k] {m n : ℕ} (M : Matrix (Fin m) (Fin n) k) : Module.finrank k ↥(tangentSpace M) = n - M.rank

theorem TangentSpaces.jacobian_rank_add_tangent_dim {k : Type u_1} [Field k] {m n : ℕ} (M : Matrix (Fin m) (Fin n) k) : M.rank + Module.finrank k ↥(tangentSpace M) = n

theorem TangentSpaces.jacobian_rank_le {k : Type u_1} [Field k] {m n : ℕ} (M : Matrix (Fin m) (Fin n) k) : M.rank ≤ n

theorem TangentSpaces.tangentSpace_jacobian_eq_tangentSpaceIdeal {k : Type u_1} [Field k] {n m : ℕ} (f : Fin m → MvPolynomial (Fin n) k) (P : Fin n → k) (hP : ∀ g ∈ Ideal.span (Set.range f), (MvPolynomial.eval P) g = 0) : tangentSpace (jacobianMatrix n m f P) = tangentSpaceIdeal (Ideal.span (Set.range f)) P

theorem TangentSpaces.rank_le_one_of_single_row {k : Type u_1} [Field k] {n : ℕ} (M : Matrix (Fin 1) (Fin n) k) : M.rank ≤ 1

theorem function_field_generated_by_n_plus_one (k : Type u_1) (F : Type u_2) [Field k] [IsAlgClosed k] [Field F] [Algebra k F] (n : ℕ) (hfg : ⊤.FG) (htrdeg : Algebra.trdeg k F = ↑n) : ∃ (α : Fin (n + 1) → F), (AlgebraicIndependent k fun (i : Fin n) => α i.castSucc) ∧ IntermediateField.adjoin k (Set.range α) = ⊤

def IsHypersurface (k : Type u_1) [Field k] (N : ℕ) (W : Set (AffineSpace_k k N)) : Prop

theorem coordinateRingBar_isDomain' (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffineSpace_k k N)) (hV : IsAffineVariety k N V) : IsDomain (AffineCoordinateRingBar V)

def functionField (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffineSpace_k k N)) (hV : IsAffineVariety k N V) : Type u_1

@[reducible]

noncomputable def functionField.instField (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffineSpace_k k N)) (hV : IsAffineVariety k N V) : Field (functionField k N V hV)

@[implicit_reducible]

noncomputable instance instFieldFunctionField (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffineSpace_k k N)) (hV : IsAffineVariety k N V) : Field (functionField k N V hV)

@[reducible]

noncomputable def functionField.instAlgebra (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffineSpace_k k N)) (hV : IsAffineVariety k N V) : Algebra (AlgebraicClosure k) (functionField k N V hV)

@[implicit_reducible]

noncomputable instance instAlgebraAlgebraicClosureFunctionField (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffineSpace_k k N)) (hV : IsAffineVariety k N V) : Algebra (AlgebraicClosure k) (functionField k N V hV)

def HasDimension (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffineSpace_k k N)) (d : ℕ) : Prop

theorem functionField_fg (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffineSpace_k k N)) (hV : IsAffineVariety k N V) : ⊤.FG

noncomputable def rationalMapPullback (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (φ : RationalMap k M N V W) (hdom : RationalMap.IsDominant k φ) : functionField k N W hW →ₐ[AlgebraicClosure k] functionField k M V hV

theorem affineRationalMap_to_dominant_rationalMap (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) [IsDomain (AffineCoordinateRingBar V)] [IsDomain (AffineCoordinateRingBar W)] (φ : AffineRationalMap V W) (hdom : IsDominantRationalMap W φ) : ∃ (ψ : RationalMap k M N V W), RationalMap.IsDominant k ψ

noncomputable def algHomInducesDominantRationalMap (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (θ : functionField k N W hW →ₐ[AlgebraicClosure k] functionField k M V hV) : ∃ (ψ : RationalMap k M N V W), RationalMap.IsDominant k ψ

theorem theorem_15_8_iii_forward (k : Type u_1) [Field k] (M N P : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (Z : Set (AffineSpace_k k P)) (hZ : IsAffineVariety k P Z) (φ : RationalMap k M N V W) (hφdom : RationalMap.IsDominant k φ) (ψ : RationalMap k N P W Z) (hψdom : RationalMap.IsDominant k ψ) (ψφ : RationalMap k M P V Z) (hψφdom : RationalMap.IsDominant k ψφ) (hcomp : ∀ Q ∈ RationalMap.compDom k ψ φ, RationalMap.toFun k ψ (RationalMap.toFun k φ Q) = RationalMap.toFun k ψφ Q) : rationalMapPullback k M P V hV Z hZ ψφ hψφdom = (rationalMapPullback k M N V hV W hW φ hφdom).comp (rationalMapPullback k N P W hW Z hZ ψ hψdom)

theorem rationalMapPullback_roundtrip_points (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (φ : RationalMap k M N V W) (hdom : RationalMap.IsDominant k φ) (ψ : RationalMap k M N V W) (hψdom : RationalMap.IsDominant k ψ) (hψ : ∃ (_ : RationalMap.IsDominant k ψ), ψ = ⋯.choose) (P : AffineSpace_k k M) : P ∈ RationalMap.dom k φ ∩ RationalMap.dom k ψ → RationalMap.toFun k φ P = RationalMap.toFun k ψ P

theorem algHom_roundtrip (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (θ : functionField k N W hW →ₐ[AlgebraicClosure k] functionField k M V hV) : rationalMapPullback k M N V hV W hW ⋯.choose ⋯ = θ

theorem pullback_comp_of_birational_eq_id (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (φ : RationalMap k M N V W) (ψ : RationalMap k N M W V) (hφdom : RationalMap.IsDominant k φ) (hψdom : RationalMap.IsDominant k ψ) (hcomp1 : ∀ P ∈ RationalMap.compDom k ψ φ, RationalMap.toFun k ψ (RationalMap.toFun k φ P) = P) (hcomp2 : ∀ P ∈ RationalMap.compDom k φ ψ, RationalMap.toFun k φ (RationalMap.toFun k ψ P) = P) : (rationalMapPullback k N M W hW V hV ψ hψdom).comp (rationalMapPullback k M N V hV W hW φ hφdom) = AlgHom.id (AlgebraicClosure k) (functionField k N W hW)

theorem pullback_comp_of_birational_eq_id' (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (φ : RationalMap k M N V W) (ψ : RationalMap k N M W V) (hφdom : RationalMap.IsDominant k φ) (hψdom : RationalMap.IsDominant k ψ) (hcomp1 : ∀ P ∈ RationalMap.compDom k ψ φ, RationalMap.toFun k ψ (RationalMap.toFun k φ P) = P) (hcomp2 : ∀ P ∈ RationalMap.compDom k φ ψ, RationalMap.toFun k φ (RationalMap.toFun k ψ P) = P) : (rationalMapPullback k M N V hV W hW φ hφdom).comp (rationalMapPullback k N M W hW V hV ψ hψdom) = AlgHom.id (AlgebraicClosure k) (functionField k M V hV)

theorem inverse_algHom_induces_inverse_rationalMap (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (θ1 : functionField k N W hW →ₐ[AlgebraicClosure k] functionField k M V hV) (θ2 : functionField k M V hV →ₐ[AlgebraicClosure k] functionField k N W hW) (hcomp : θ2.comp θ1 = AlgHom.id (AlgebraicClosure k) (functionField k N W hW)) : have φ := ⋯.choose; have hφ := ⋯; have ψ := ⋯.choose; have hψ := ⋯; ∀ P ∈ RationalMap.compDom k ψ φ, RationalMap.toFun k ψ (RationalMap.toFun k φ P) = P

theorem algEquiv_induces_birational (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (iso : functionField k M V hV ≃ₐ[AlgebraicClosure k] functionField k N W hW) : IsBirationallyEquivalent k V W

theorem birational_of_functionField_iso (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (iso : functionField k M V hV ≃ₐ[AlgebraicClosure k] functionField k N W hW) : IsBirationallyEquivalent k V W

theorem functionField_iso_of_birational (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) (hbir : IsBirationallyEquivalent k V W) : Nonempty (functionField k M V hV ≃ₐ[AlgebraicClosure k] functionField k N W hW)

theorem birational_iff_functionField_iso (k : Type u_1) [Field k] (M N : ℕ) (V : Set (AffineSpace_k k M)) (hV : IsAffineVariety k M V) (W : Set (AffineSpace_k k N)) (hW : IsAffineVariety k N W) : IsBirationallyEquivalent k V W ↔ Nonempty (functionField k M V hV ≃ₐ[AlgebraicClosure k] functionField k N W hW)

theorem irreducible_poly_vanishing_on_generators_axiom (k : Type u_1) [Field k] [IsAlgClosed k] (n : ℕ) (F : Type u_2) [Field F] [Algebra (AlgebraicClosure k) F] (α : Fin (n + 1) → F) (h_indep : AlgebraicIndependent (AlgebraicClosure k) fun (i : Fin n) => α i.castSucc) (h_gen : IntermediateField.adjoin (AlgebraicClosure k) (Set.range α) = ⊤) : ∃ (f : MvPolynomial (Fin (n + 1)) (AlgebraicClosure k)), Irreducible f ∧ (MvPolynomial.aeval α) f = 0

theorem irreducible_poly_vanishing_on_generators (k : Type u_1) [Field k] [IsAlgClosed k] (n : ℕ) (F : Type u_2) [Field F] [Algebra (AlgebraicClosure k) F] (α : Fin (n + 1) → F) (h_indep : AlgebraicIndependent (AlgebraicClosure k) fun (i : Fin n) => α i.castSucc) (h_gen : IntermediateField.adjoin (AlgebraicClosure k) (Set.range α) = ⊤) (h_not_indep : ¬AlgebraicIndependent (AlgebraicClosure k) α) : ∃ (f : MvPolynomial (Fin (n + 1)) (AlgebraicClosure k)), Irreducible f ∧ (MvPolynomial.aeval α) f = 0

theorem nullstellensatz_irreducible (k : Type u_1) [Field k] [IsAlgClosed k] (N : ℕ) (f : MvPolynomial (Fin N) (AlgebraicClosure k)) (hf_irred : Irreducible f) : idealOfAlgebraicSet (AlgebraicSet k N {f}) = Ideal.span {f}

theorem functionField_iso_of_irreducible_vanishing (k : Type u_1) [Field k] [IsAlgClosed k] (n : ℕ) (F : Type u_2) [Field F] [Algebra (AlgebraicClosure k) F] (α : Fin (n + 1) → F) (h_gen : IntermediateField.adjoin (AlgebraicClosure k) (Set.range α) = ⊤) (f : MvPolynomial (Fin (n + 1)) (AlgebraicClosure k)) (hf_irred : Irreducible f) (hf_vanish : (MvPolynomial.aeval α) f = 0) (hW : IsAffineVariety k (n + 1) (AlgebraicSet k (n + 1) {f})) : Nonempty (F ≃ₐ[AlgebraicClosure k] functionField k (n + 1) (AlgebraicSet k (n + 1) {f}) hW)

theorem hypersurface_from_generators (k : Type u_1) [Field k] [IsAlgClosed k] (n : ℕ) (F : Type u_2) [Field F] [Algebra (AlgebraicClosure k) F] (α : Fin (n + 1) → F) (h_indep : AlgebraicIndependent (AlgebraicClosure k) fun (i : Fin n) => α i.castSucc) (h_gen : IntermediateField.adjoin (AlgebraicClosure k) (Set.range α) = ⊤) (h_not_indep : ¬AlgebraicIndependent (AlgebraicClosure k) α) : ∃ (f : MvPolynomial (Fin (n + 1)) (AlgebraicClosure k)), Irreducible f ∧ ∀ (hW : IsAffineVariety k (n + 1) (AlgebraicSet k (n + 1) {f})), Nonempty (F ≃ₐ[AlgebraicClosure k] functionField k (n + 1) (AlgebraicSet k (n + 1) {f}) hW)

theorem hypersurface_isAffineVariety (k : Type u_1) [Field k] (N : ℕ) (f : MvPolynomial (Fin N) (AlgebraicClosure k)) (hf : Irreducible f) : IsAffineVariety k N (AlgebraicSet k N {f})

theorem isHypersurface_of_irreducible (k : Type u_1) [Field k] [IsAlgClosed k] (N : ℕ) (f : MvPolynomial (Fin N) (AlgebraicClosure k)) (hf : Irreducible f) : IsHypersurface k N (AlgebraicSet k N {f})

theorem IsHypersurface.exists_irreducible {k : Type u_1} [Field k] {N : ℕ} {W : Set (AffineSpace_k k N)} (hW : IsHypersurface k N W) : ∃ (f : MvPolynomial (Fin N) (AlgebraicClosure k)), Irreducible f ∧ W = AlgebraicSet k N {f}

theorem variety_birational_to_hypersurface (k : Type u_1) [Field k] [IsAlgClosed k] (N n : ℕ) (V : Set (AffineSpace_k k N)) (hV : HasDimension k N V n) : ∃ (W : Set (AffineSpace_k k (n + 1))), IsHypersurface k (n + 1) W ∧ IsBirationallyEquivalent k V W

theorem trdeg_lemma_17_7_axiom_helper (k' : Type u_1) [Field k'] (N : ℕ) (hN : N ≥ 1) (I : Ideal (MvPolynomial (Fin N) k')) (hI : I.IsPrime) (hprinc : ∃ (f : MvPolynomial (Fin N) k'), Irreducible f ∧ I = Ideal.span {f}) [inst_dom : IsDomain (MvPolynomial (Fin N) k' ⧸ I)] : Algebra.trdeg k' (FractionRing (MvPolynomial (Fin N) k' ⧸ I)) = ↑(N - 1)

theorem trdeg_fractionRing_mvPoly_quotient_prime_principal (k' : Type u_1) [Field k'] (N : ℕ) (hN : N ≥ 1) (I : Ideal (MvPolynomial (Fin N) k')) (hI : I.IsPrime) (hprinc : ∃ (f : MvPolynomial (Fin N) k'), Irreducible f ∧ I = Ideal.span {f}) [inst_dom : IsDomain (MvPolynomial (Fin N) k' ⧸ I)] : Algebra.trdeg k' (FractionRing (MvPolynomial (Fin N) k' ⧸ I)) = ↑(N - 1)

theorem hypersurface_trdeg_eq (k : Type u_1) [Field k] (N : ℕ) (hN : N ≥ 1) (f : MvPolynomial (Fin N) (AlgebraicClosure k)) (hf : Irreducible f) (hV : IsAffineVariety k N (AlgebraicSet k N {f})) : Algebra.trdeg (AlgebraicClosure k) (functionField k N (AlgebraicSet k N {f}) hV) = ↑(N - 1)

theorem hypersurface_has_dimension_n_minus_one (k : Type u_1) [Field k] (N : ℕ) (hN : N ≥ 1) (V : Set (AffineSpace_k k N)) (hV : IsHypersurface k N V) : HasDimension k N V (N - 1)

def affinePartOfProjective (k : Type u_1) [Field k] {n : ℕ} (V : Set (Projectivization (AlgebraicClosure k) (Fin (n + 1) → AlgebraicClosure k))) (i : Fin (n + 1)) : Set (Fin n → AlgebraicClosure k)

def IsProjectiveHypersurface (k : Type u_1) [Field k] {n : ℕ} (V : Set (Projectivization (AlgebraicClosure k) (Fin (n + 1) → AlgebraicClosure k))) : Prop

def HasProjectiveDimension (k : Type u_1) [Field k] {n : ℕ} (V : Set (Projectivization (AlgebraicClosure k) (Fin (n + 1) → AlgebraicClosure k))) (d : ℕ) : Prop

theorem projective_hypersurface_has_affine_part (k : Type u_1) [Field k] [IsAlgClosed k] (n : ℕ) (hn : n ≥ 1) (V : Set (Projectivization (AlgebraicClosure k) (Fin (n + 1) → AlgebraicClosure k))) (hV : IsProjectiveHypersurface k V) : ∃ (i : Fin (n + 1)), IsHypersurface k n (affinePartOfProjective k V i) ∧ HasDimension k n (affinePartOfProjective k V i) (n - 1)

theorem tangent_dim_ge_variety_dim (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : Fin n → AlgebraicClosure k) (hP : P ∈ AlgebraicSet k n (Set.range f)) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) : Module.finrank (AlgebraicClosure k) ↥(TangentSpaces.tangentSpace (TangentSpaces.jacobianMatrix n m f P)) ≥ d

theorem dim_le_ambient (k : Type u_1) [Field k] (N d : ℕ) (V : Set (AffineSpace_k k N)) (hdim : HasDimension k N V d) : d ≤ N

theorem corollary_17_11_rank_bound (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : Fin n → AlgebraicClosure k) (hP : P ∈ AlgebraicSet k n (Set.range f)) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) : (TangentSpaces.jacobianMatrix n m f P).rank ≤ n - d

theorem jacobian_rank_le_codim (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : Fin n → AlgebraicClosure k) (hP : P ∈ AlgebraicSet k n (Set.range f)) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) : (TangentSpaces.jacobianMatrix n m f P).rank ≤ n - d ∧ d ≤ n

theorem SingularLocus.rank_lt_iff_all_minors_det_eq_zero {k' : Type u_2} [Field k'] {m n r : ℕ} (M : Matrix (Fin m) (Fin n) k') : M.rank < r ↔ ∀ (ri : Fin r → Fin m) (ci : Fin r → Fin n), (M.submatrix ri ci).det = 0

noncomputable def SingularLocus.jacobianPolyMatrix (k : Type u_1) [Field k] (n m : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) : Matrix (Fin m) (Fin n) (MvPolynomial (Fin n) (AlgebraicClosure k))

def SingularLocus.minorDetPolys (k : Type u_1) [Field k] (n m r : ℕ) (M : Matrix (Fin m) (Fin n) (MvPolynomial (Fin n) (AlgebraicClosure k))) : Set (MvPolynomial (Fin n) (AlgebraicClosure k))

theorem SingularLocus.eval_minor_det_eq (k : Type u_1) [Field k] (n m r : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : Fin n → AlgebraicClosure k) (ri : Fin r → Fin m) (ci : Fin r → Fin n) : (MvPolynomial.eval P) ((jacobianPolyMatrix k n m f).submatrix ri ci).det = ((TangentSpaces.jacobianMatrix n m f P).submatrix ri ci).det

def SingularLocus.singularLocusIntrinsic (k : Type u_1) [Field k] (n m r : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) : Set (AffineSpace_k k n)

def SingularLocus.singularLocusPolys (k : Type u_1) [Field k] (n m r : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) : Set (MvPolynomial (Fin n) (AlgebraicClosure k))

def SingularLocus.singularLocusAlgebraic (k : Type u_1) [Field k] (n m r : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) : Set (AffineSpace_k k n)

theorem SingularLocus.mem_singularLocusAlgebraic_iff (k : Type u_1) [Field k] (n m r : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : AffineSpace_k k n) : P ∈ singularLocusAlgebraic k n m r f ↔ (∀ (i : Fin m), (MvPolynomial.eval P) (f i) = 0) ∧ ∀ (ri : Fin r → Fin m) (ci : Fin r → Fin n), ((TangentSpaces.jacobianMatrix n m f P).submatrix ri ci).det = 0

theorem SingularLocus.singularLocus_eq_algebraicSet (k : Type u_1) [Field k] (n m r : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) : singularLocusIntrinsic k n m r f = singularLocusAlgebraic k n m r f

theorem SingularLocus.singular_locus_is_closed_subset (k : Type u_2) [Field k] (n m r : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) : IsAlgebraicSubset k n (singularLocusIntrinsic k n m r f) ∧ singularLocusIntrinsic k n m r f ⊆ AlgebraicSet k n (Set.range f)

theorem SingularLocus.hypersurface_smooth_point (k : Type u_1) [Field k] (d : ℕ) (g : MvPolynomial (Fin (d + 1)) (AlgebraicClosure k)) (hg : Irreducible g) (hW : IsAffineVariety k (d + 1) (AlgebraicSet k (d + 1) {g})) : ∃ P ∈ AlgebraicSet k (d + 1) {g}, ¬(TangentSpaces.jacobianMatrix (d + 1) 1 (fun (x : Fin 1) => g) P).rank < 1

theorem SingularLocus.birational_preserves_smooth_locus (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (hV : IsAffineVariety k n (AlgebraicSet k n (Set.range f))) (hdimV : HasDimension k n (AlgebraicSet k n (Set.range f)) d) (hyp_smooth : ∀ (g : MvPolynomial (Fin (d + 1)) (AlgebraicClosure k)), Irreducible g → IsAffineVariety k (d + 1) (AlgebraicSet k (d + 1) {g}) → ∃ Q ∈ AlgebraicSet k (d + 1) {g}, ¬(TangentSpaces.jacobianMatrix (d + 1) 1 (fun (x : Fin 1) => g) Q).rank < 1) : ∃ P ∈ AlgebraicSet k n (Set.range f), ¬(TangentSpaces.jacobianMatrix n m f P).rank < n - d

theorem SingularLocus.jacobian_rank_achieves_codim (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (hV : IsAffineVariety k n (AlgebraicSet k n (Set.range f))) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) : ∃ P ∈ AlgebraicSet k n (Set.range f), ¬(TangentSpaces.jacobianMatrix n m f P).rank < n - d

theorem SingularLocus.nonvanishing_minor_exists (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (hV : IsAffineVariety k n (AlgebraicSet k n (Set.range f))) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) : ∃ (ri : Fin (n - d) → Fin m) (ci : Fin (n - d) → Fin n), ∃ P ∈ AlgebraicSet k n (Set.range f), ((TangentSpaces.jacobianMatrix n m f P).submatrix ri ci).det ≠ 0

theorem SingularLocus.variety_has_smooth_point (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (hV : IsAffineVariety k n (AlgebraicSet k n (Set.range f))) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) : ∃ P ∈ AlgebraicSet k n (Set.range f), ¬(TangentSpaces.jacobianMatrix n m f P).rank < n - d

theorem SingularLocus.singularLocus_proper (k : Type u_1) [Field k] (n m r d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (hV : IsAffineVariety k n (AlgebraicSet k n (Set.range f))) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) (hr : r = n - d) : singularLocusIntrinsic k n m r f ≠ AlgebraicSet k n (Set.range f)

theorem SingularLocus.singular_locus_is_proper_closed_subset (k : Type u_2) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (hV : IsAffineVariety k n (AlgebraicSet k n (Set.range f))) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) : have r := n - d; have SingV := singularLocusIntrinsic k n m r f; IsAlgebraicSubset k n SingV ∧ SingV ⊆ AlgebraicSet k n (Set.range f) ∧ SingV ≠ AlgebraicSet k n (Set.range f)

theorem cotangent_finrank_eq_derivation_finrank {R : Type u_1} [CommRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] [Algebra R k] [IsScalarTower k R k] (e : Module.Dual k (IsLocalRing.CotangentSpace R) ≃ₗ[k] Derivation k R k) : Module.finrank k (IsLocalRing.CotangentSpace R) = Module.finrank k (Derivation k R k)

def IsSmoothPoint (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : Fin n → AlgebraicClosure k) : Prop

theorem corollary_17_14_jacobian_rank (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : Fin n → AlgebraicClosure k) (hP : P ∈ AlgebraicSet k n (Set.range f)) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) : ¬(TangentSpaces.jacobianMatrix n m f P).rank < n - d ↔ Module.finrank (AlgebraicClosure k) ↥(TangentSpaces.tangentSpace (TangentSpaces.jacobianMatrix n m f P)) = d

theorem corollary_17_14 (k : Type u_1) [Field k] (n m d : ℕ) (f : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (P : Fin n → AlgebraicClosure k) (hP : P ∈ AlgebraicSet k n (Set.range f)) (hdim : HasDimension k n (AlgebraicSet k n (Set.range f)) d) {R : Type u_2} [CommRing R] [IsLocalRing R] [Algebra (AlgebraicClosure k) R] [Algebra R (AlgebraicClosure k)] [IsScalarTower (AlgebraicClosure k) R (AlgebraicClosure k)] (e : Module.Dual (AlgebraicClosure k) (IsLocalRing.CotangentSpace R) ≃ₗ[AlgebraicClosure k] Derivation (AlgebraicClosure k) R (AlgebraicClosure k)) (h_tangent_eq : Module.finrank (AlgebraicClosure k) (Derivation (AlgebraicClosure k) R (AlgebraicClosure k)) = Module.finrank (AlgebraicClosure k) ↥(TangentSpaces.tangentSpace (TangentSpaces.jacobianMatrix n m f P))) : ¬(TangentSpaces.jacobianMatrix n m f P).rank < n - d ↔ Module.finrank (AlgebraicClosure k) (IsLocalRing.CotangentSpace R) = d