Module

IntermediateField_isDomain_tensorProduct_of_le_laurentSeries.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IntermediateField_isDomain_tensorProduct_of_le_laurentSeries

8 declarations indexed from sourceView source ↗

Module documentation

Intermediate Field is Domain tensor Product of le laurent Series

Imports2

Nyll.AlgebraicCurves.FunctionFields.LaurentBaseChange
Mathlib.RingTheory.LinearDisjoint

Imported by2

theorem

algebraMap_laurent

L31 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IntermediateField_isDomain_tensorProduct_of_le_laurentSeries.RegExt.algebraMap_laurent

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IntermediateField_isDomain_tensorProduct_of_le_laurentSeries
open scoped TensorProduct
namespace RegExt
variable (κ k : Type*) [Field κ] [Field k] [Algebra κ k]

Lean source · statement

theorem algebraMap_laurent (c : κ) :
    algebraMap κ (LaurentSeries k) c = HahnSeries.C (algebraMap κ k c)

def

coeffAlgHom

L38 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IntermediateField_isDomain_tensorProduct_of_le_laurentSeries.RegExt.coeffAlgHom

Documentation

The algebra map on Laurent series induced by extension of the coefficient field.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IntermediateField_isDomain_tensorProduct_of_le_laurentSeries
open scoped TensorProduct
namespace RegExt
variable (κ k : Type*) [Field κ] [Field k] [Algebra κ k]

Lean source · statement

def coeffAlgHom : LaurentSeries κ →ₐ[κ] LaurentSeries k

theorem

coeffAlgHom_coeff

L47 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IntermediateField_isDomain_tensorProduct_of_le_laurentSeries.RegExt.coeffAlgHom_coeff

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IntermediateField_isDomain_tensorProduct_of_le_laurentSeries
open scoped TensorProduct
namespace RegExt
variable (κ k : Type*) [Field κ] [Field k] [Algebra κ k]

Lean source · statement

theorem coeffAlgHom_coeff (x : LaurentSeries κ) (n : ℤ) :
    (coeffAlgHom κ k x).coeff n = algebraMap κ k (x.coeff n)

def

constAlgHom

L51 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IntermediateField_isDomain_tensorProduct_of_le_laurentSeries.RegExt.constAlgHom

Documentation

The algebra map sending a field element to its constant Laurent series.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IntermediateField_isDomain_tensorProduct_of_le_laurentSeries
open scoped TensorProduct
namespace RegExt
variable (κ k : Type*) [Field κ] [Field k] [Algebra κ k]

Lean source · statement

def constAlgHom : k →ₐ[κ] LaurentSeries k

theorem

constAlgHom_apply

L57 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IntermediateField_isDomain_tensorProduct_of_le_laurentSeries.RegExt.constAlgHom_apply

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IntermediateField_isDomain_tensorProduct_of_le_laurentSeries
open scoped TensorProduct
namespace RegExt
variable (κ k : Type*) [Field κ] [Field k] [Algebra κ k]

Lean source · statement

theorem constAlgHom_apply (b : k) : constAlgHom κ k b = HahnSeries.C b

theorem

linearDisjoint_range

L59 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IntermediateField_isDomain_tensorProduct_of_le_laurentSeries.RegExt.linearDisjoint_range

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IntermediateField_isDomain_tensorProduct_of_le_laurentSeries
open scoped TensorProduct
namespace RegExt
variable (κ k : Type*) [Field κ] [Field k] [Algebra κ k]

Lean source · statement

theorem linearDisjoint_range :
    (coeffAlgHom κ k).range.LinearDisjoint (constAlgHom κ k).range

theorem

isDomain

L102 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IntermediateField_isDomain_tensorProduct_of_le_laurentSeries.RegExt.isDomain

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IntermediateField_isDomain_tensorProduct_of_le_laurentSeries
open scoped TensorProduct
namespace RegExt

Lean source · statement

theorem isDomain (κ k : Type*) [Field κ] [Field k] [Algebra κ k] (R : IntermediateField κ
  (LaurentSeries κ)) :
    IsDomain (↥R ⊗[κ] k)

theorem

isDomain_tensorProduct_of_le_laurentSeries

L118 ↗

IntermediateField.isDomain_tensorProduct_of_le_laurentSeries

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IntermediateField_isDomain_tensorProduct_of_le_laurentSeries
open scoped TensorProduct

Lean source · statement

theorem _root_.IntermediateField.isDomain_tensorProduct_of_le_laurentSeries
    (κ : Type*) [Field κ] (k : Type*) [Field k] [Algebra κ k]
    (R : IntermediateField κ (LaurentSeries κ)) :
    IsDomain (↥R ⊗[κ] k)

Module documentation

Intermediate Field is Domain tensor Product of le laurent Series

Declarations