NYLL
Module

LinearMap_bijective_and_flip_bijective_of_baseChange_residueField.lean

Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_bijective_and_flip_bijective_of_baseChange_residueField
5 declarations indexed from sourceView source ↗

Module documentation

Linear Map bijective and flip bijective of base Change residue Field

Imports7
  • Mathlib.LinearAlgebra.Dual.Lemmas
  • Mathlib.RingTheory.FiniteType
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • Mathlib.RingTheory.Nakayama
  • Mathlib.RingTheory.TensorProduct.Finite
  • Mathlib.RingTheory.TensorProduct.Free
  • Mathlib.Tactic.Abel
Imported by1

Declarations

theorem

exists_apply_eq_of_baseChange_residueField

L43 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_bijective_and_flip_bijective_of_baseChange_residueField.BaseChangeResidueFieldPerfect.exists_apply_eq_of_baseChange_residueField
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_bijective_and_flip_bijective_of_baseChange_residueField
open scoped TensorProduct
open Module
universe u v w₁ w₂ w₁' w₂'
namespace BaseChangeResidueFieldPerfect
section
variable {R : Type u} [CommRing R] [IsLocalRing R] {k : Type v} [Field k] [Algebra R k]
    {M : Type w₁} {N : Type w₂} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    {Mk : Type w₁'} {Nk : Type w₂'} [AddCommGroup Mk] [Module k Mk] [AddCommGroup Nk] [Module k Nk]
omit [IsLocalRing R] in
Lean source · statement
theorem exists_apply_eq_of_baseChange_residueField
    (hπ : Function.Surjective (algebraMap R k))
    (B : M →ₗ[R] N →ₗ[R] R) (Bk : Mk →ₗ[k] Nk →ₗ[k] k)
    (eM : k ⊗[R] M ≃ₗ[k] Mk) (eN : k ⊗[R] N ≃ₗ[k] Nk)
    (hcomp : ∀ m n, Bk (eM (1 ⊗ₜ[R] m)) (eN (1 ⊗ₜ[R] n)) = algebraMap R k (B m n))
    (y : k ⊗[R] M) : ∃ m : M, ∀ n : N, Bk (eM y) (eN (1 ⊗ₜ[R] n)) = algebraMap R k (B m n)
theorem

surjective_of_baseChange_residueField

L64 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_bijective_and_flip_bijective_of_baseChange_residueField.BaseChangeResidueFieldPerfect.surjective_of_baseChange_residueField
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_bijective_and_flip_bijective_of_baseChange_residueField
open scoped TensorProduct
open Module
universe u v w₁ w₂ w₁' w₂'
namespace BaseChangeResidueFieldPerfect
section
variable {R : Type u} [CommRing R] [IsLocalRing R] {k : Type v} [Field k] [Algebra R k]
    {M : Type w₁} {N : Type w₂} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    {Mk : Type w₁'} {Nk : Type w₂'} [AddCommGroup Mk] [Module k Mk] [AddCommGroup Nk] [Module k Nk]
Lean source · statement
theorem surjective_of_baseChange_residueField [Module.Free R N] [Module.Finite R N]
    (hπ : Function.Surjective (algebraMap R k))
    (B : M →ₗ[R] N →ₗ[R] R) (Bk : Mk →ₗ[k] Nk →ₗ[k] k)
    (eM : k ⊗[R] M ≃ₗ[k] Mk) (eN : k ⊗[R] N ≃ₗ[k] Nk)
    (hcomp : ∀ m n, Bk (eM (1 ⊗ₜ[R] m)) (eN (1 ⊗ₜ[R] n)) = algebraMap R k (B m n))
    (hBk : Function.Surjective Bk) :
    Function.Surjective B
theorem

finrank_eq_of_baseChange_residueField

L105 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_bijective_and_flip_bijective_of_baseChange_residueField.BaseChangeResidueFieldPerfect.finrank_eq_of_baseChange_residueField
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_bijective_and_flip_bijective_of_baseChange_residueField
open scoped TensorProduct
open Module
universe u v w₁ w₂ w₁' w₂'
namespace BaseChangeResidueFieldPerfect
section
variable {R : Type u} [CommRing R] [IsLocalRing R] {k : Type v} [Field k] [Algebra R k]
    {M : Type w₁} {N : Type w₂} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    {Mk : Type w₁'} {Nk : Type w₂'} [AddCommGroup Mk] [Module k Mk] [AddCommGroup Nk] [Module k Nk]
Lean source · statement
theorem finrank_eq_of_baseChange_residueField [Module.Free R M] [Module.Finite R M]
    [Module.Free R N] [Module.Finite R N]
    (Bk : Mk →ₗ[k] Nk →ₗ[k] k) (eM : k ⊗[R] M ≃ₗ[k] Mk) (eN : k ⊗[R] N ≃ₗ[k] Nk)
    (hBk : Function.Bijective Bk ∧ Function.Bijective Bk.flip) :
    Module.finrank R M = Module.finrank R N
theorem

bijective_and_flip_bijective_of_baseChange_residueField

L122 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.LinearMap_bijective_and_flip_bijective_of_baseChange_residueField.BaseChangeResidueFieldPerfect.bijective_and_flip_bijective_of_baseChange_residueField
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_bijective_and_flip_bijective_of_baseChange_residueField
open scoped TensorProduct
open Module
universe u v w₁ w₂ w₁' w₂'
namespace BaseChangeResidueFieldPerfect
section
variable {R : Type u} [CommRing R] [IsLocalRing R] {k : Type v} [Field k] [Algebra R k]
    {M : Type w₁} {N : Type w₂} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    {Mk : Type w₁'} {Nk : Type w₂'} [AddCommGroup Mk] [Module k Mk] [AddCommGroup Nk] [Module k Nk]
Lean source · statement
theorem bijective_and_flip_bijective_of_baseChange_residueField
    [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N]
    (hπ : Function.Surjective (algebraMap R k))
    (B : M →ₗ[R] N →ₗ[R] R) (Bk : Mk →ₗ[k] Nk →ₗ[k] k)
    (eM : k ⊗[R] M ≃ₗ[k] Mk) (eN : k ⊗[R] N ≃ₗ[k] Nk)
    (hcomp : ∀ m n, Bk (eM (1 ⊗ₜ[R] m)) (eN (1 ⊗ₜ[R] n)) = algebraMap R k (B m n))
    (hBk : Function.Bijective Bk ∧ Function.Bijective Bk.flip) :
    Function.Bijective B ∧ Function.Bijective B.flip
theorem

bijective_and_flip_bijective_of_baseChange_residueField

L153 ↗
LinearMap.bijective_and_flip_bijective_of_baseChange_residueField
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace LinearMap_bijective_and_flip_bijective_of_baseChange_residueField
open scoped TensorProduct
open Module
universe u v w₁ w₂ w₁' w₂'
Lean source · statement
theorem _root_.LinearMap.bijective_and_flip_bijective_of_baseChange_residueField
    {R : Type u} [CommRing R] [IsLocalRing R] {k : Type v} [Field k] [Algebra R k]
    {M : Type w₁} {N : Type w₂} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    {Mk : Type w₁'} {Nk : Type w₂'} [AddCommGroup Mk] [Module k Mk] [AddCommGroup Nk] [Module k Nk]
    [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N]
    (hπ : Function.Surjective (algebraMap R k))
    (B : M →ₗ[R] N →ₗ[R] R) (Bk : Mk →ₗ[k] Nk →ₗ[k] k)
    (eM : k ⊗[R] M ≃ₗ[k] Mk) (eN : k ⊗[R] N ≃ₗ[k] Nk)
    (hcomp : ∀ m n, Bk (eM (1 ⊗ₜ[R] m)) (eN (1 ⊗ₜ[R] n)) = algebraMap R k (B m n))
    (hBk : Function.Bijective Bk ∧ Function.Bijective Bk.flip) :
    Function.Bijective B ∧ Function.Bijective B.flip

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