Module

InvertibleModule.lean

Nyll.SchemeTheory.RingTheory.Descent.InvertibleModule

10 declarations indexed from sourceView source ↗

Module documentation

Module Invertible of invertible tensor Product of faithfully Flat

Imports16

Mathlib.Algebra.Module.NatInt
Mathlib.Algebra.Module.Projective
Mathlib.Algebra.Module.FinitePresentation
Mathlib.LinearAlgebra.Contraction
Mathlib.LinearAlgebra.Dual.Defs
Mathlib.LinearAlgebra.Dual.BaseChange
Mathlib.LinearAlgebra.TensorProduct.Defs
Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.RingTheory.Finiteness.Cardinality
Mathlib.RingTheory.Finiteness.Descent
Mathlib.RingTheory.Flat.Equalizer
Mathlib.RingTheory.Flat.EquationalCriterion
Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Mathlib.RingTheory.PicardGroup
Mathlib.RingTheory.TensorProduct.Basic

Imported by2

def

dualBC

L51 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat.S17FF.dualBC

Documentation

The base-change comparison from the tensor product of the dual to the dual after base change.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
namespace S17FF
section DualBaseChange
variable {R : Type*} [CommRing R] (S : Type*) [CommRing S] [Algebra R S]
  (M : Type*) [AddCommGroup M] [Module R M]
  {N : Type*} [AddCommGroup N] [Module R N]

Lean source · statement

def dualBC : S ⊗[R] Module.Dual R M →ₗ[S] Module.Dual S (S ⊗[R] M)

theorem

dualBC_tmul

L54 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat.S17FF.dualBC_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
namespace S17FF
section DualBaseChange
variable {R : Type*} [CommRing R] (S : Type*) [CommRing S] [Algebra R S]
  (M : Type*) [AddCommGroup M] [Module R M]
  {N : Type*} [AddCommGroup N] [Module R N]

Lean source · statement

theorem dualBC_tmul (s : S) (f : Module.Dual R M) :
    dualBC S M (s ⊗ₜ f) = s • f.baseChange S

theorem

dualBC_natural

L59 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat.S17FF.dualBC_natural

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
namespace S17FF
section DualBaseChange
variable {R : Type*} [CommRing R] (S : Type*) [CommRing S] [Algebra R S]
  (M : Type*) [AddCommGroup M] [Module R M]
  {N : Type*} [AddCommGroup N] [Module R N]
variable {M} in

Lean source · statement

theorem dualBC_natural (u : M →ₗ[R] N) (z : S ⊗[R] Module.Dual R N) :
    dualBC S M (u.dualMap.lTensor S z) = (dualBC S N z) ∘ₗ u.baseChange S

theorem

dualBC_bijective_of_free

L69 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat.S17FF.dualBC_bijective_of_free

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
namespace S17FF
section DualBaseChange
variable {R : Type*} [CommRing R] (S : Type*) [CommRing S] [Algebra R S]
  (M : Type*) [AddCommGroup M] [Module R M]
  {N : Type*} [AddCommGroup N] [Module R N]
variable {M} in

Lean source · statement

theorem dualBC_bijective_of_free [Module.Free R M] [Module.Finite R M] :
    Function.Bijective (dualBC (R := R) S M)

theorem

dualBC_bijective_of_projective

L91 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat.S17FF.dualBC_bijective_of_projective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
namespace S17FF
section DualBaseChange
variable {R : Type*} [CommRing R] (S : Type*) [CommRing S] [Algebra R S]
  (M : Type*) [AddCommGroup M] [Module R M]
  {N : Type*} [AddCommGroup N] [Module R N]
variable {M} in

Lean source · statement

theorem dualBC_bijective_of_projective [Module.Projective R M] [Module.Finite R M] :
    Function.Bijective (dualBC (R := R) S M)

theorem

bijective_of_lTensor_bijective

L122 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat.S17FF.bijective_of_lTensor_bijective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
namespace S17FF
section Descent
variable {R : Type*} [CommRing R] (S : Type*) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
  {M : Type*} [AddCommGroup M] [Module R M]
omit [Module.FaithfullyFlat R S] in

Lean source · statement

theorem bijective_of_lTensor_bijective [Module.FaithfullyFlat R S] {N P : Type*} [AddCommMonoid N]
    [Module R N] [AddCommMonoid P] [Module R P] (f : N →ₗ[R] P)
    (h : Function.Bijective (f.lTensor S)) : Function.Bijective f

theorem

finitePresentation_of_faithfullyFlat

L129 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat.S17FF.finitePresentation_of_faithfullyFlat

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
namespace S17FF
section Descent
variable {R : Type*} [CommRing R] (S : Type*) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
  {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

theorem finitePresentation_of_faithfullyFlat [Module.FinitePresentation S (S ⊗[R] M)] :
    Module.FinitePresentation R M

theorem

projective_of_faithfullyFlat

L152 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat.S17FF.projective_of_faithfullyFlat

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
namespace S17FF
section Descent
variable {R : Type*} [CommRing R] (S : Type*) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
  {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

theorem projective_of_faithfullyFlat [Module.Finite S (S ⊗[R] M)]
    [Module.Projective S (S ⊗[R] M)] : Module.Projective R M

theorem

invertible_of_faithfullyFlat

L160 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat.S17FF.invertible_of_faithfullyFlat

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Invertible_of_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
namespace S17FF
section Descent
variable {R : Type*} [CommRing R] (S : Type*) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
  {M : Type*} [AddCommGroup M] [Module R M]

Lean source · statement

theorem invertible_of_faithfullyFlat [Module.Invertible S (S ⊗[R] M)] :
    Module.Invertible R M

theorem

of_invertible_tensorProduct_of_faithfullyFlat

L204 ↗

Module.Invertible.of_invertible_tensorProduct_of_faithfullyFlat

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_invertible_tensorProduct_of_faithfullyFlat
open TensorProduct
universe u v w

Lean source · statement

theorem _root_.Module.Invertible.of_invertible_tensorProduct_of_faithfullyFlat
    {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S]
    {M : Type w} [AddCommGroup M] [Module R M]
    [Module.Invertible S (TensorProduct R S M)] :
    Module.Invertible R M

Module documentation

Module Invertible of invertible tensor Product of faithfully Flat

Declarations