Module

Module_Projective_exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_Projective_exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat

3 declarations indexed from sourceView source ↗

Module documentation

Lift compatible projective-module identifications across a square-zero quotient.

Imports8

Mathlib.Algebra.Module.Projective
Mathlib.LinearAlgebra.TensorProduct.Quotient
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.Nakayama
Mathlib.RingTheory.Nilpotent.Basic
Mathlib.RingTheory.TensorProduct.Basic
Mathlib.Tactic.Abel
Mathlib.Tactic.Ring.RingNF

Imported by2

lemma

le_jacobson_bot_of_sq_eq_bot_aux

L36 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Projective_exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat.le_jacobson_bot_of_sq_eq_bot_aux

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Projective_exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat
universe u
open TensorProduct
open scoped _root_.Module _root_.Module.Projective in

Lean source · statement

lemma le_jacobson_bot_of_sq_eq_bot_aux
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I ^ 2 = ⊥) :
    I ≤ (⊥ : Ideal R).jacobson

lemma

surjective_of_one_tmul_aux

L54 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Projective_exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat.surjective_of_one_tmul_aux

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Projective_exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat
universe u
open TensorProduct
open scoped _root_.Module _root_.Module.Projective in

Lean source · statement

lemma surjective_of_one_tmul_aux
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I ≤ (⊥ : Ideal R).jacobson)
    {N M : Type u} [AddCommGroup N] [AddCommGroup M] [Module R N] [Module R M]
    [Module.Finite R M] (f : N →ₗ[R] M)
    (hf : ∀ m : M, ∃ n : N, (1 : R ⧸ I) ⊗ₜ[R] f n = (1 : R ⧸ I) ⊗ₜ[R] m) :
    Function.Surjective f

theorem

exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat

L77 ↗

Module.Projective.exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Projective_exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat
universe u
open TensorProduct

Lean source · statement

theorem _root_.Module.Projective.exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I ^ 2 = ⊥)
    (P₁ P₂ : Type u) [AddCommGroup P₁] [AddCommGroup P₂] [Module R P₁] [Module R P₂]
    [Module.Projective R P₁] [Module.Finite R P₁]
    [Module.Projective R P₂] [Module.Finite R P₂]
    (e : ((R ⧸ I) ⊗[R] P₁) ≃ₗ[R ⧸ I] ((R ⧸ I) ⊗[R] P₂)) :
    ∃ σ' : P₁ ≃ₗ[R] P₂, ∀ p : P₁, (1 : R ⧸ I) ⊗ₜ[R] σ' p = e ((1 : R ⧸ I) ⊗ₜ[R] p)

Module documentation

Declarations

le_jacobson_bot_of_sq_eq_bot_aux

surjective_of_one_tmul_aux

exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat