NYLL
Module

Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
10 declarations indexed from sourceView source ↗

Module documentation

Module ker base Change le range and finrank eq of field extension

Imports5
Imported by1

Declarations

def

incl

L39 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.K4EDescendGood.incl
Documentation

The scalar-restricted inclusion of the smaller field into its extension.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
namespace K4EDescendGood
variable {R : Type u} [CommRing R] (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K']
  [Algebra R K']
  [Algebra K K'] [IsScalarTower R K K']
Lean source · statement
def incl : K →ₗ[R] K'
theorem

exists_retraction

L41 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.K4EDescendGood.exists_retraction
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
namespace K4EDescendGood
variable {R : Type u} [CommRing R] (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K']
  [Algebra R K']
  [Algebra K K'] [IsScalarTower R K K']
Lean source · statement
theorem exists_retraction : ∃ r : K' →ₗ[K] K, r ∘ₗ Algebra.linearMap K K' = LinearMap.id
theorem

baseChange_j

L47 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.K4EDescendGood.baseChange_j
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
namespace K4EDescendGood
variable {R : Type u} [CommRing R] (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K']
  [Algebra R K']
  [Algebra K K'] [IsScalarTower R K K']
variable {X Y : Type u} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
Lean source · statement
theorem baseChange_j (φ : X →ₗ[R] Y) (z : K ⊗[R] X) :
    φ.baseChange K' ((incl K K').rTensor X z) = (incl K K').rTensor Y (φ.baseChange K z)
theorem

baseChange_ρ

L53 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.K4EDescendGood.baseChange_ρ
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
namespace K4EDescendGood
variable {R : Type u} [CommRing R] (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K']
  [Algebra R K']
  [Algebra K K'] [IsScalarTower R K K']
variable {X Y : Type u} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
Lean source · statement
theorem baseChange_ρ (r : K' →ₗ[K] K) (φ : X →ₗ[R] Y) (z : K' ⊗[R] X) :
    φ.baseChange K ((r.restrictScalars R).rTensor X z) = (r.restrictScalars R).rTensor Y
      (φ.baseChange K' z)
theorem

ρ_j

L61 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.K4EDescendGood.ρ_j
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
namespace K4EDescendGood
variable {R : Type u} [CommRing R] (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K']
  [Algebra R K']
  [Algebra K K'] [IsScalarTower R K K']
variable {X Y : Type u} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
Lean source · statement
theorem ρ_j (r : K' →ₗ[K] K) (hr : r ∘ₗ Algebra.linearMap K K' = LinearMap.id) (z : K ⊗[R] X) :
    (r.restrictScalars R).rTensor X ((incl K K').rTensor X z) = z
theorem

ker_le_range_descend

L69 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.K4EDescendGood.ker_le_range_descend
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
namespace K4EDescendGood
variable {R : Type u} [CommRing R] (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K']
  [Algebra R K']
  [Algebra K K'] [IsScalarTower R K K']
variable {X Y : Type u} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
Lean source · statement
theorem ker_le_range_descend {Z : Type u} [AddCommGroup Z] [Module R Z]
    (f : X →ₗ[R] Y) (g : Y →ₗ[R] Z)
    (h : LinearMap.ker (g.baseChange K') ≤ LinearMap.range (f.baseChange K')) :
    LinearMap.ker (g.baseChange K) ≤ LinearMap.range (f.baseChange K)
theorem

cancelBaseChange_baseChange_baseChange

L82 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.K4EDescendGood.cancelBaseChange_baseChange_baseChange
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
namespace K4EDescendGood
variable {R : Type u} [CommRing R] (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K']
  [Algebra R K']
  [Algebra K K'] [IsScalarTower R K K']
variable {X Y : Type u} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
Lean source · statement
theorem cancelBaseChange_baseChange_baseChange (φ : X →ₗ[R] Y) (z : K' ⊗[K] (K ⊗[R] X)) :
    AlgebraTensorModule.cancelBaseChange R K K' K' Y (((φ.baseChange K).baseChange K') z) =
      (φ.baseChange K') (AlgebraTensorModule.cancelBaseChange R K K' K' X z)
theorem

finrank_baseChange_field

L93 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.K4EDescendGood.finrank_baseChange_field
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
namespace K4EDescendGood
variable {R : Type u} [CommRing R] (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K']
  [Algebra R K']
  [Algebra K K'] [IsScalarTower R K K']
variable {X Y : Type u} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
omit [Algebra R K] [Algebra R K'] [IsScalarTower R K K'] in
Lean source · statement
theorem finrank_baseChange_field (V : Type u) [AddCommGroup V] [Module K V] :
    Module.finrank K' (K' ⊗[K] V) = Module.finrank K V
theorem

finrank_ker_descend

L97 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension.K4EDescendGood.finrank_ker_descend
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
namespace K4EDescendGood
variable {R : Type u} [CommRing R] (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K']
  [Algebra R K']
  [Algebra K K'] [IsScalarTower R K K']
variable {X Y : Type u} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
Lean source · statement
theorem finrank_ker_descend (φ : X →ₗ[R] Y) :
    Module.finrank K' (LinearMap.ker (φ.baseChange K')) = Module.finrank K (LinearMap.ker
      (φ.baseChange K))
theorem

ker_baseChange_le_range_and_finrank_eq_of_field_extension

L120 ↗
Module.ker_baseChange_le_range_and_finrank_eq_of_field_extension
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
universe u
open TensorProduct
open K4EDescendGood in
Lean source · statement
theorem _root_.Module.ker_baseChange_le_range_and_finrank_eq_of_field_extension
    {R : Type u} [CommRing R]
    (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
    (d : ∀ i, C i →ₗ[R] C (i + 1))
    {F : Type u} [AddCommGroup F] [Module R F] (Θ : F →ₗ[R] C 0)
    (K : Type u) [Field K] [Algebra R K] (K' : Type u) [Field K'] [Algebra R K'] [Algebra K K']
    [IsScalarTower R K K'] (r : ℕ)
    (h1 : ∀ i : ℕ, LinearMap.ker ((d (i + 1)).baseChange K') ≤ LinearMap.range ((d i).baseChange
      K'))
    (h2 : LinearMap.ker ((d 0).baseChange K') ≤ LinearMap.range (Θ.baseChange K'))
    (h3 : Module.finrank K' (LinearMap.ker ((d 0).baseChange K')) = r) :
    (∀ i : ℕ, LinearMap.ker ((d (i + 1)).baseChange K) ≤ LinearMap.range ((d i).baseChange K)) ∧
    LinearMap.ker ((d 0).baseChange K) ≤ LinearMap.range (Θ.baseChange K) ∧
    Module.finrank K (LinearMap.ker ((d 0).baseChange K)) = r

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.