Module

IntermediateField_finrank_adjoin_range_le_finrank_of_transcendental.lean

Nyll.AlgebraicCurves.Foundations.FieldTheory.IntermediateField_finrank_adjoin_range_le_finrank_of_transcendental

3 declarations indexed from sourceView source ↗

Module documentation

Intermediate Field finrank adjoin range le finrank of transcendental

Imports1

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Imported by1

Nyll.AlgebraicCurves.Foundations.FieldTheory.All

theorem

rho_mem_adjoin

L39 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_finrank_adjoin_range_le_finrank_of_transcendental.DBResdeg.rho_mem_adjoin

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_finrank_adjoin_range_le_finrank_of_transcendental
open scoped TensorProduct Polynomial
open IntermediateField
universe u
noncomputable section
namespace DBResdeg
variable {𝔽 : Type u} [Field 𝔽] {k : Type u} [Field k] [Algebra 𝔽 k]
  {κ : Type u} [Field κ] [Algebra 𝔽 κ] [Algebra 𝔽[X] κ] [IsScalarTower 𝔽 𝔽[X] κ]
  {Ω : Type u} [Field Ω] [Algebra k Ω] [Algebra 𝔽 Ω] [IsScalarTower 𝔽 k Ω]
  (ρ : κ →ₐ[𝔽] Ω)
omit [IsScalarTower 𝔽 𝔽[X] κ] in

Lean source · statement

theorem rho_mem_adjoin (c : ↥(IntermediateField.adjoin 𝔽 ({algebraMap 𝔽[X] κ Polynomial.X} : Set
  κ))) :
    ρ (c : κ) ∈ IntermediateField.adjoin k ({ρ (algebraMap 𝔽[X] κ Polynomial.X)} : Set Ω)

theorem

finrank_le_card

L49 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.IntermediateField_finrank_adjoin_range_le_finrank_of_transcendental.DBResdeg.finrank_le_card

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_finrank_adjoin_range_le_finrank_of_transcendental
open scoped TensorProduct Polynomial
open IntermediateField
universe u
noncomputable section
namespace DBResdeg
variable {𝔽 : Type u} [Field 𝔽] {k : Type u} [Field k] [Algebra 𝔽 k]
  {κ : Type u} [Field κ] [Algebra 𝔽 κ] [Algebra 𝔽[X] κ] [IsScalarTower 𝔽 𝔽[X] κ]
  {Ω : Type u} [Field Ω] [Algebra k Ω] [Algebra 𝔽 Ω] [IsScalarTower 𝔽 k Ω]
  (ρ : κ →ₐ[𝔽] Ω)
omit [IsScalarTower 𝔽 𝔽[X] κ] in

Lean source · statement

theorem finrank_le_card
    (hfin : FiniteDimensional ↥(IntermediateField.adjoin 𝔽 ({algebraMap 𝔽[X] κ Polynomial.X} : Set
      κ)) κ)
    {ιy : Type*} [Fintype ιy]
    (y : Module.Basis ιy ↥(IntermediateField.adjoin 𝔽 ({algebraMap 𝔽[X] κ Polynomial.X} : Set κ))
      κ) :
    Module.finrank ↥(IntermediateField.adjoin k ({⟨ρ (algebraMap 𝔽[X] κ Polynomial.X),
          IntermediateField.subset_adjoin k (Set.range ρ) ⟨_, rfl⟩⟩} : Set
            ↥(IntermediateField.adjoin k (Set.range ρ))))
        ↥(IntermediateField.adjoin k (Set.range ρ)) ≤ Fintype.card ιy

theorem

finrank_adjoin_range_le_finrank_of_transcendental

L141 ↗

IntermediateField.finrank_adjoin_range_le_finrank_of_transcendental

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace IntermediateField_finrank_adjoin_range_le_finrank_of_transcendental
open scoped TensorProduct Polynomial
open IntermediateField
universe u
noncomputable section
open DBResdeg in

Lean source · statement

theorem _root_.IntermediateField.finrank_adjoin_range_le_finrank_of_transcendental
    (𝔽 : Type u) [Field 𝔽] (k : Type u) [Field k] [Algebra 𝔽 k]
    (κ : Type u) [Field κ] [Algebra 𝔽 κ] [Algebra 𝔽[X] κ] [IsScalarTower 𝔽 𝔽[X] κ]
    (hfin : FiniteDimensional ↥(IntermediateField.adjoin 𝔽 ({algebraMap 𝔽[X] κ Polynomial.X} : Set
      κ)) κ)
    (Ω : Type u) [Field Ω] [Algebra k Ω] [Algebra 𝔽 Ω] [IsScalarTower 𝔽 k Ω]
    (ρ : κ →ₐ[𝔽] Ω) (_htr : Transcendental k (ρ (algebraMap 𝔽[X] κ Polynomial.X))) :
    Module.finrank ↥(IntermediateField.adjoin k ({⟨ρ (algebraMap 𝔽[X] κ Polynomial.X),
          IntermediateField.subset_adjoin k (Set.range ρ) ⟨_, rfl⟩⟩} : Set
            ↥(IntermediateField.adjoin k (Set.range ρ))))
        ↥(IntermediateField.adjoin k (Set.range ρ)) ≤
      Module.finrank ↥(IntermediateField.adjoin 𝔽 ({algebraMap 𝔽[X] κ Polynomial.X} : Set κ)) κ

Module documentation

Intermediate Field finrank adjoin range le finrank of transcendental

Declarations

rho_mem_adjoin

finrank_le_card

finrank_adjoin_range_le_finrank_of_transcendental