Module

LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.lean

Nyll.AlgebraicCurves.Foundations.Algebra.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le

19 declarations indexed from sourceView source ↗

Module documentation

Linear Equiv exists forall finrank inf map pow add finrank inf le

Imports13

Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.Algebra.Polynomial.Monic
Mathlib.Data.Finset.Lattice.Fold
Mathlib.LinearAlgebra.FiniteDimensional.Defs
Mathlib.LinearAlgebra.FiniteDimensional.Basic
Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Mathlib.LinearAlgebra.Prod
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Noetherian.Defs
Mathlib.Tactic.Abel
Mathlib.Tactic.Choose
Mathlib.Tactic.Ext

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

theorem

map_pow_le

L42 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.map_pow_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]

Lean source · statement

theorem map_pow_le {ψ : W →ₗ[k] W} {S : Submodule k W} (hS : S.map ψ ≤ S) :
    ∀ M : ℕ, S.map (ψ^M) ≤ S

theorem

mem_of_pow_map

L50 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.mem_of_pow_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]

Lean source · statement

theorem mem_of_pow_map {ψ : W →ₗ[k] W} {S : Submodule k W} (hS : S.map ψ ≤ S)
    (M : ℕ) {x : W} (hx : x ∈ S) : (ψ^M) x ∈ S

def

barEnd

L56 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.barEnd

Documentation

The endomorphism induced on the quotient of the invariant submodule by its intersection with the other.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]

Lean source · statement

def barEnd (φ : W →ₗ[k] W) (P B : Submodule k W)
    (hP : P.map φ ≤ P) (hB : B.map φ ≤ B) :
    (B ⧸ P.comap B.subtype) →ₗ[k] (B ⧸ P.comap B.subtype)

theorem

finiteDimensional_quot_of_monicTorsion

L62 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.finiteDimensional_quot_of_monicTorsion

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]

Lean source · statement

theorem finiteDimensional_quot_of_monicTorsion
    (φ : W →ₗ[k] W) (P B : Submodule k W)
    (hP : P.map φ ≤ P) (hB : B.map φ ≤ B)
    (S : Submodule k W) (hSB : S ≤ B) [FiniteDimensional k S]
    (hgen : B ≤ ⨆ j : ℕ, S.map (φ ^ j))
    (htor : ∀ y ∈ B, ∃ c : Polynomial k, c.Monic ∧ Polynomial.aeval φ c y ∈ P) :
    FiniteDimensional k (B ⧸ P.comap B.subtype)

theorem

disjoint_ker_pow_range_pow_aux

L143 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.disjoint_ker_pow_range_pow_aux

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]

Lean source · statement

theorem disjoint_ker_pow_range_pow_aux {V : Type*} [AddCommGroup V] [Module k V]
    [FiniteDimensional k V] (g : V →ₗ[k] V) :
    ∃ M₀, ∀ M ≥ M₀, Disjoint (LinearMap.ker (g^M)) (LinearMap.range (g^M))

theorem

fitting_step

L159 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.fitting_step

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]

Lean source · statement

theorem fitting_step
    {V₁ V₂ : Type*} [AddCommGroup V₁] [Module k V₁] [FiniteDimensional k V₁]
    [AddCommGroup V₂] [Module k V₂] [FiniteDimensional k V₂]
    (f : V₁ →ₗ[k] V₁) (g : V₂ →ₗ[k] V₂) (S : Submodule k (V₁ × V₂)) :
    ∃ M₀, ∀ M ≥ M₀,
      Module.finrank k S ≤
        Module.finrank k ↥(S.map (LinearMap.prodMap (f ^ M) LinearMap.id) ⊔
          S.map (LinearMap.prodMap LinearMap.id (g ^ M)))

theorem

aux_symm_mul

L217 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.aux_symm_mul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem aux_symm_mul : (φ.symm : W →ₗ[k] W) * (φ : W →ₗ[k] W) = 1

theorem

aux_mul_symm

L220 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.aux_mul_symm

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem aux_mul_symm : (φ : W →ₗ[k] W) * (φ.symm : W →ₗ[k] W) = 1

theorem

pow_symm_pow

L223 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.pow_symm_pow

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem pow_symm_pow (M : ℕ) (x : W) :
    ((φ.symm : W →ₗ[k] W) ^ M) (((φ : W →ₗ[k] W) ^ M) x) = x

theorem

pow_pow_symm

L234 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.pow_pow_symm

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem pow_pow_symm (M : ℕ) (x : W) :
    ((φ : W →ₗ[k] W) ^ M) (((φ.symm : W →ₗ[k] W) ^ M) x) = x

theorem

barEnd_mkQ

L238 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.barEnd_mkQ

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem barEnd_mkQ (ψ : W →ₗ[k] W) (P B : Submodule k W)
    (hP : P.map ψ ≤ P) (hB : B.map ψ ≤ B) (x : W) (hx : x ∈ B) :
    barEnd ψ P B hP hB ((P.comap B.subtype).mkQ ⟨x, hx⟩) =
      (P.comap B.subtype).mkQ ⟨ψ x, hB ⟨x, hx, rfl⟩⟩

theorem

barEnd_pow_mkQ

L245 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.barEnd_pow_mkQ

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem barEnd_pow_mkQ (ψ : W →ₗ[k] W) (P B : Submodule k W)
    (hP : P.map ψ ≤ P) (hB : B.map ψ ≤ B) (M : ℕ) (x : W) (hx : x ∈ B) :
    ((barEnd ψ P B hP hB) ^ M) ((P.comap B.subtype).mkQ ⟨x, hx⟩) =
      (P.comap B.subtype).mkQ ⟨(ψ^M) x, mem_of_pow_map hB M hx⟩

theorem

symm_pow_mem_of_mem_map

L259 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.symm_pow_mem_of_mem_map

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem symm_pow_mem_of_mem_map (M : ℕ) (x : W) (hx : x ∈ B'.map ((φ : W →ₗ[k] W) ^ M)) :
    ((φ.symm : W →ₗ[k] W) ^ M) x ∈ B'

def

Psi

L265 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.Psi

Documentation

The map to the two quotient spaces, using inclusion and the inverse power of the given equivalence.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

def Psi (M : ℕ) :
    ↥(B ⊓ B'.map ((φ : W →ₗ[k] W) ^ M)) →ₗ[k]
      (B ⧸ P.comap B.subtype) × (B' ⧸ P'.comap B'.subtype)

theorem

ker_Psi_eq

L275 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.ker_Psi_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem ker_Psi_eq (_hPB : P ≤ B) (_hP'B' : P' ≤ B') (M : ℕ) :
    LinearMap.ker (Psi φ P B P' B' M) =
      (P ⊓ P'.map ((φ : W →ₗ[k] W) ^ M)).comap
        (B ⊓ B'.map ((φ : W →ₗ[k] W) ^ M)).subtype

theorem

Psi_fst

L303 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.Psi_fst

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem Psi_fst (M : ℕ) (z : ↥(B ⊓ B'.map ((φ : W →ₗ[k] W) ^ M))) :
    (Psi φ P B P' B' M z).1 = (P.comap B.subtype).mkQ ⟨z.1, z.2.1⟩

theorem

Psi_snd

L306 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.Psi_snd

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem Psi_snd (M : ℕ) (z : ↥(B ⊓ B'.map ((φ : W →ₗ[k] W) ^ M))) :
    (Psi φ P B P' B' M z).2 =
      (P'.comap B'.subtype).mkQ ⟨((φ.symm:W→ₗ[k]W)^M) z.1,
        symm_pow_mem_of_mem_map φ B' M z.1 z.2.2⟩

theorem

range_Psi_superset

L311 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le.Ef8d.range_Psi_superset

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
namespace Ef8d
variable {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
variable (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W)

Lean source · statement

theorem range_Psi_superset
    (hP : P.map (φ : W →ₗ[k] W) ≤ P) (hB : B.map (φ : W →ₗ[k] W) ≤ B)
    (hP' : P'.map (φ.symm : W →ₗ[k] W) ≤ P') (hB' : B'.map (φ.symm : W →ₗ[k] W) ≤ B')
    (M : ℕ) :
    (LinearMap.range (Psi φ P B P' B' 0)).map
        (LinearMap.prodMap ((barEnd (φ : W →ₗ[k] W) P B hP hB) ^ M) LinearMap.id) ⊔
      (LinearMap.range (Psi φ P B P' B' 0)).map
        (LinearMap.prodMap LinearMap.id ((barEnd (φ.symm : W →ₗ[k] W) P' B' hP' hB') ^ M))
      ≤ LinearMap.range (Psi φ P B P' B' M)

theorem

exists_forall_finrank_inf_map_pow_add_finrank_inf_le

L353 ↗

LinearEquiv.exists_forall_finrank_inf_map_pow_add_finrank_inf_le

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
noncomputable section
open Submodule LinearMap Module
open Ef8d in

Lean source · statement

theorem _root_.LinearEquiv.exists_forall_finrank_inf_map_pow_add_finrank_inf_le
    {k : Type*} [Field k] {W : Type*} [AddCommGroup W] [Module k W]
    (φ : W ≃ₗ[k] W) (P B P' B' : Submodule k W) (hPB : P ≤ B) (hP'B' : P' ≤ B')
    (hP : P.map (φ : W →ₗ[k] W) ≤ P) (hB : B.map (φ : W →ₗ[k] W) ≤ B)
    (hP' : P'.map (φ.symm : W →ₗ[k] W) ≤ P') (hB' : B'.map (φ.symm : W →ₗ[k] W) ≤ B')
    (hfin : ∀ M : ℕ, FiniteDimensional k ↥(B ⊓ B'.map ((φ : W →ₗ[k] W) ^ M)))
    (hgen : ∃ M₁ : ℕ, B ≤ ⨆ j : ℕ,
      (B ⊓ B'.map ((φ : W →ₗ[k] W) ^ M₁)).map ((φ : W →ₗ[k] W) ^ j))
    (hgen' : ∃ M₁ : ℕ, B' ≤ ⨆ j : ℕ,
      (B' ⊓ B.map ((φ.symm : W →ₗ[k] W) ^ M₁)).map ((φ.symm : W →ₗ[k] W) ^ j))
    (htor : ∀ y ∈ B, ∃ c : Polynomial k, c.Monic ∧
      Polynomial.aeval (φ : W →ₗ[k] W) c y ∈ P)
    (htor' : ∀ y ∈ B', ∃ c : Polynomial k, c.Monic ∧
      Polynomial.aeval (φ.symm : W →ₗ[k] W) c y ∈ P') :
    ∃ M₀ : ℕ, ∀ M : ℕ, M₀ ≤ M →
      Module.finrank k ↥(P ⊓ P'.map ((φ : W →ₗ[k] W) ^ M)) + Module.finrank k ↥(B ⊓ B') ≤
        Module.finrank k ↥(B ⊓ B'.map ((φ : W →ₗ[k] W) ^ M)) +
          Module.finrank k ↥(P ⊓ P')

Module documentation

Linear Equiv exists forall finrank inf map pow add finrank inf le

Declarations