NYLL
Module

Module_Invertible_of_projective_of_forall_finrank_eq_one.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_Invertible_of_projective_of_forall_finrank_eq_one
7 declarations indexed from sourceView source ↗

Module documentation

Invertibility of projective modules of rank one

Shows that a finite projective module with one-dimensional fibers is invertible.

Imports7
  • Mathlib.LinearAlgebra.Dual.BaseChange
  • Mathlib.RingTheory.PicardGroup
  • Mathlib.Tactic.Conv
  • Mathlib.Tactic.Ext
  • Mathlib.Tactic.Ring.RingNF
  • Mathlib.Tactic.SimpRw
  • Mathlib.Tactic.TermCongr
Imported by7

Declarations

lemma

mul_comm_of_equiv

L45 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_projective_of_forall_finrank_eq_one.Module.Invertible.RankOneAux.mul_comm_of_equiv
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_projective_of_forall_finrank_eq_one
universe u v
open TensorProduct
namespace Module
open _root_.Module
namespace Invertible
namespace RankOneAux
open _root_.Module.Invertible
open _root_.Module
variable {A : Type u} [CommRing A] {P : Type v} [AddCommGroup P] [Module A P]
Lean source · statement
lemma mul_comm_of_equiv {B : Type*} [CommRing B] {L : Type*} [AddCommGroup L] [Module B L]
    (e : B ≃ₗ[B] L) (f g : Module.Dual B L) (l l' : L) : f l * g l' = f l' * g l
lemma

finrank_localization_eq_one

L59 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_projective_of_forall_finrank_eq_one.Module.Invertible.RankOneAux.finrank_localization_eq_one
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_projective_of_forall_finrank_eq_one
universe u v
open TensorProduct
namespace Module
open _root_.Module
namespace Invertible
namespace RankOneAux
open _root_.Module.Invertible
open _root_.Module
variable {A : Type u} [CommRing A] {P : Type v} [AddCommGroup P] [Module A P]
variable [Module.Finite A P] [Module.Projective A P]
  (h : ∀ (K : Type u) [Field K] [Algebra A K], Module.finrank K (TensorProduct A K P) = 1)
include h in
Lean source · statement
lemma finrank_localization_eq_one (m : Ideal A) [m.IsMaximal] :
    Module.finrank (Localization.AtPrime m) (Localization.AtPrime m ⊗[A] P) = 1
lemma

apply_mul_apply_comm

L73 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_projective_of_forall_finrank_eq_one.Module.Invertible.RankOneAux.apply_mul_apply_comm
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_projective_of_forall_finrank_eq_one
universe u v
open TensorProduct
namespace Module
open _root_.Module
namespace Invertible
namespace RankOneAux
open _root_.Module.Invertible
open _root_.Module
variable {A : Type u} [CommRing A] {P : Type v} [AddCommGroup P] [Module A P]
variable [Module.Finite A P] [Module.Projective A P]
  (h : ∀ (K : Type u) [Field K] [Algebra A K], Module.finrank K (TensorProduct A K P) = 1)
include h in
Lean source · statement
lemma apply_mul_apply_comm (φ ψ : Module.Dual A P) (p q : P) : φ p * ψ q = φ q * ψ p
lemma

exists_dualBasis

L90 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_projective_of_forall_finrank_eq_one.Module.Invertible.RankOneAux.exists_dualBasis
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_projective_of_forall_finrank_eq_one
universe u v
open TensorProduct
namespace Module
open _root_.Module
namespace Invertible
namespace RankOneAux
open _root_.Module.Invertible
open _root_.Module
variable {A : Type u} [CommRing A] {P : Type v} [AddCommGroup P] [Module A P]
variable [Module.Finite A P] [Module.Projective A P]
  (h : ∀ (K : Type u) [Field K] [Algebra A K], Module.finrank K (TensorProduct A K P) = 1)
omit h in
Lean source · statement
lemma exists_dualBasis :
    ∃ (n : ℕ) (x : Fin n → P) (φ : Fin n → Module.Dual A P), ∀ p : P, ∑ i, φ i p • x i = p
lemma

surjective_contractLeft

L103 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_projective_of_forall_finrank_eq_one.Module.Invertible.RankOneAux.surjective_contractLeft
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_projective_of_forall_finrank_eq_one
universe u v
open TensorProduct
namespace Module
open _root_.Module
namespace Invertible
namespace RankOneAux
open _root_.Module.Invertible
open _root_.Module
variable {A : Type u} [CommRing A] {P : Type v} [AddCommGroup P] [Module A P]
variable [Module.Finite A P] [Module.Projective A P]
  (h : ∀ (K : Type u) [Field K] [Algebra A K], Module.finrank K (TensorProduct A K P) = 1)
include h in
Lean source · statement
lemma surjective_contractLeft : Function.Surjective (contractLeft A P)
lemma

injective_contractLeft

L123 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_projective_of_forall_finrank_eq_one.Module.Invertible.RankOneAux.injective_contractLeft
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_projective_of_forall_finrank_eq_one
universe u v
open TensorProduct
namespace Module
open _root_.Module
namespace Invertible
namespace RankOneAux
open _root_.Module.Invertible
open _root_.Module
variable {A : Type u} [CommRing A] {P : Type v} [AddCommGroup P] [Module A P]
variable [Module.Finite A P] [Module.Projective A P]
  (h : ∀ (K : Type u) [Field K] [Algebra A K], Module.finrank K (TensorProduct A K P) = 1)
include h in
Lean source · statement
lemma injective_contractLeft : Function.Injective (contractLeft A P)
theorem

of_projective_of_forall_finrank_eq_one

L147 ↗
Module.Invertible.of_projective_of_forall_finrank_eq_one
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_projective_of_forall_finrank_eq_one
universe u v
open TensorProduct
Lean source · statement
theorem _root_.Module.Invertible.of_projective_of_forall_finrank_eq_one
    {A : Type u} [CommRing A] (P : Type v) [AddCommGroup P] [Module A P]
    [Module.Finite A P] [Module.Projective A P]
    (h : ∀ (K : Type u) [Field K] [Algebra A K], Module.finrank K (TensorProduct A K P) = 1) :
    Module.Invertible A P

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