Module

Geometric.lean

Nyll.SchemeTheory.PlaneCurves.Geometric

5 declarations indexed from sourceView source ↗

Module documentation

Field Arithmetic, Chapter 6: plane curves

This file starts the source-producing infrastructure for Section 6.1: scalar extension to an algebraic closure and the zero sets of multivariate polynomials.

Imports3

Mathlib.Algebra.MvPolynomial.Eval
Mathlib.Algebra.MvPolynomial.Nilpotent
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Imported by2

def

mapToAlgebraicClosure

L28 ↗

FieldArithmetic.Chapter06.mapToAlgebraicClosure

Documentation

Extend the coefficients of a multivariate polynomial to an algebraic closure.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
universe u v
variable {K : Type u} [Field K]

Lean source · statement

def mapToAlgebraicClosure {σ : Type*} (f : MvPolynomial σ K) :
    MvPolynomial σ (AlgebraicClosure K)

def

IsAbsolutelyIrreducible

L33 ↗

FieldArithmetic.Chapter06.IsAbsolutelyIrreducible

Documentation

Absolute irreducibility, expressed over a fixed algebraic closure.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
universe u v
variable {K : Type u} [Field K]

Lean source · statement

def IsAbsolutelyIrreducible {σ : Type*} (f : MvPolynomial σ K) : Prop

theorem

irreducible

L40 ↗

FieldArithmetic.Chapter06.IsAbsolutelyIrreducible.irreducible

Documentation

An absolutely irreducible polynomial is already irreducible over its original coefficient field.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem IsAbsolutelyIrreducible.irreducible
    {σ : Type*} {f : MvPolynomial σ K}
    (hf : IsAbsolutelyIrreducible f) :
    Irreducible f

def

affineZeroSet

L78 ↗

FieldArithmetic.Chapter06.affineZeroSet

Documentation

The zero set of a multivariate polynomial after applying a coefficient map.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
universe u v
variable {K : Type u} [Field K]

Lean source · statement

def affineZeroSet {σ : Type*} {R : Type u} {S : Type v}
    [CommSemiring R] [CommSemiring S] (φ : R →+* S) (f : MvPolynomial σ R) :
    Set (σ → S)

def

geometricZeroSet

L84 ↗

FieldArithmetic.Chapter06.geometricZeroSet

Documentation

The geometric zero set of a polynomial over a fixed algebraic closure.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FieldArithmetic
namespace Chapter06
open MvPolynomial
universe u v
variable {K : Type u} [Field K]

Lean source · statement

def geometricZeroSet {σ : Type*} (f : MvPolynomial σ K) :
    Set (σ → AlgebraicClosure K)

Module documentation

Field Arithmetic, Chapter 6: plane curves

Declarations

mapToAlgebraicClosure

IsAbsolutelyIrreducible

irreducible

affineZeroSet

geometricZeroSet