Module

IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental.lean

Nyll.AlgebraicCurves.Foundations.FieldTheory.IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental

8 declarations indexed from sourceView source ↗

Module documentation

Is Alg Closed exists alg Equiv apply eq add algebra Map of transcendental

Imports4

Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Mathlib.Tactic.Conv

Imported by2

def

shift

L34 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental.TranslateTranscendental.shift

Documentation

The polynomial algebra map translating each variable by the corresponding scalar.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
open MvPolynomial
namespace TranslateTranscendental
variable {K : Type*} [Field K] {ι : Type*}

Lean source · statement

def shift (c : ι → K) : MvPolynomial ι K →ₐ[K] MvPolynomial ι K

theorem

shift_X

L37 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental.TranslateTranscendental.shift_X

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
open MvPolynomial
namespace TranslateTranscendental
variable {K : Type*} [Field K] {ι : Type*}

Lean source · statement

theorem shift_X (c : ι → K) (i : ι) : shift c (X i) = X i + C (c i)

theorem

shift_comp_shift_neg

L40 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental.TranslateTranscendental.shift_comp_shift_neg

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
open MvPolynomial
namespace TranslateTranscendental
variable {K : Type*} [Field K] {ι : Type*}

Lean source · statement

theorem shift_comp_shift_neg (c : ι → K) : (shift c).comp (shift (-c)) = AlgHom.id K _

theorem

shift_neg_comp_shift

L45 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental.TranslateTranscendental.shift_neg_comp_shift

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
open MvPolynomial
namespace TranslateTranscendental
variable {K : Type*} [Field K] {ι : Type*}

Lean source · statement

theorem shift_neg_comp_shift (c : ι → K) : (shift (-c)).comp (shift c) = AlgHom.id K _

def

shiftEquiv

L50 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental.TranslateTranscendental.shiftEquiv

Documentation

The polynomial algebra equivalence whose inverse translates each variable by the opposite scalar.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
open MvPolynomial
namespace TranslateTranscendental
variable {K : Type*} [Field K] {ι : Type*}

Lean source · statement

def shiftEquiv (c : ι → K) : MvPolynomial ι K ≃ₐ[K] MvPolynomial ι K

theorem

shiftEquiv_X

L53 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental.TranslateTranscendental.shiftEquiv_X

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
open MvPolynomial
namespace TranslateTranscendental
variable {K : Type*} [Field K] {ι : Type*}

Lean source · statement

theorem shiftEquiv_X (c : ι → K) (i : ι) : shiftEquiv c (X i) = X i + C (c i)

theorem

shiftEquiv_C

L56 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental.TranslateTranscendental.shiftEquiv_C

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
open MvPolynomial
namespace TranslateTranscendental
variable {K : Type*} [Field K] {ι : Type*}

Lean source · statement

theorem shiftEquiv_C (c : ι → K) (k : K) : shiftEquiv c (C k) = C k

theorem

exists_algEquiv_apply_eq_add_algebraMap_of_transcendental

L62 ↗

IsAlgClosed.exists_algEquiv_apply_eq_add_algebraMap_of_transcendental

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IsAlgClosed_exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
open MvPolynomial
open TranslateTranscendental in

Lean source · statement

theorem _root_.IsAlgClosed.exists_algEquiv_apply_eq_add_algebraMap_of_transcendental
    (K K' : Type*) [Field K] [Field K'] [Algebra K K'] [IsAlgClosed K']
    (t : K') (ht : Transcendental K t) (a : K) :
    ∃ τ : K' ≃ₐ[K] K', τ t = t + algebraMap K K' a

Module documentation

Is Alg Closed exists alg Equiv apply eq add algebra Map of transcendental

Declarations