Module

Module_Projective_exists_baseChange_quotient_iso_of_squareZero.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_Projective_exists_baseChange_quotient_iso_of_squareZero

1 declaration indexed from sourceView source ↗

Module documentation

Lifting projective modules across a square-zero quotient using base change.

Imports10

Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.Algebra.Module.Projective
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.LinearAlgebra.StdBasis
Mathlib.LinearAlgebra.TensorProduct.Quotient
Mathlib.RingTheory.Finiteness.Cardinality
Mathlib.Tactic.Abel
Mathlib.Tactic.Choose
Mathlib.Tactic.Conv
Mathlib.Tactic.Ring.RingNF

Imported by2

theorem

exists_baseChange_quotient_iso_of_squareZero

L37 ↗

Module.Projective.exists_baseChange_quotient_iso_of_squareZero

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_baseChange_quotient_iso_of_squareZero
universe u
open TensorProduct Polynomial

Lean source · statement

theorem _root_.Module.Projective.exists_baseChange_quotient_iso_of_squareZero
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I ^ 2 = ⊥)
    (P : Type u) [AddCommGroup P] [Module (R ⧸ I) P]
    [Module.Projective (R ⧸ I) P] [Module.Finite (R ⧸ I) P] :
    ∃ (P' : Type u) (_ : AddCommGroup P') (_ : Module R P'),
      Module.Projective R P' ∧ Module.Finite R P' ∧
      Nonempty (((R ⧸ I) ⊗[R] P') ≃ₗ[R ⧸ I] P)

Module documentation

Declarations

exists_baseChange_quotient_iso_of_squareZero