Documentation

Mathlib.RingTheory.PicardGroup

The Picard group of a commutative ring #

This file defines the Picard group CommRing.Pic R of a commutative ring R as the type of invertible R-modules (in the sense that M is invertible if there exists another R-module N such that M ⊗[R] N ≃ₗ[R] R) up to isomorphism, equipped with tensor product as multiplication.

Main definition #

Module.Invertible R M says that the canonical map Mᵛ ⊗[R] M → R is an isomorphism. To show that M is invertible, it suffices to provide an arbitrary R-module N and an isomorphism N ⊗[R] M ≃ₗ[R] R, see Module.Invertible.right.
ClassGroup.equivPic: the class group of a domain is isomorphic to the Picard group.

Main results #

An invertible module is finite and projective (provided as instances).
Module.Invertible.free_iff_linearEquiv: an invertible module is free iff it is isomorphic to the ring, i.e. its class is trivial in the Picard group.
Submodule.ker_unitsToPic, Submodule.range_unitsToPic: exactness of the sequence 1 → Rˣ → Aˣ → (Submodule R A)ˣ → Pic R → Pic A at the last two spots. See Theorem 2.4 in [RobertsSingh1993] or Exercise I.3.7(iv) and Proposition I.3.5 in [Weibel2013].

References #

https://qchu.wordpress.com/2014/10/19/the-picard-groups/
https://mathoverflow.net/questions/13768/what-is-the-right-definition-of-the-picard-group-of-a-commutative-ring
https://mathoverflow.net/questions/375725/picard-group-vs-class-group
[Weibel2013], https://sites.math.rutgers.edu/~weibel/Kbook/Kbook.I.pdf
Stacks: Picard groups of rings

TODO #

Show:

Invertible modules over a commutative ring have the same cardinality as the ring.
Establish other characterizations of invertible modules, e.g. they are modules that become free of rank one when localized at every prime ideal. See Stacks: Finite projective modules.
Connect to invertible sheaves on Spec R. More generally, connect projective R-modules of constant finite rank to locally free sheaves on Spec R.
Exhibit isomorphism with sheaf cohomology H¹(Spec R, 𝓞ˣ).

class Module.Invertible (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] :

An R-module M is invertible if the canonical map Mᵛ ⊗[R] M → R is an isomorphism, where Mᵛ is the R-dual of M.

bijective : Function.Bijective ⇑(contractLeft R M)

Instances

noncomputable def Module.Invertible.linearEquiv (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

TensorProduct R (Dual R M) M ≃ₗ[R] R

Promote the canonical map Mᵛ ⊗[R] M → R to a linear equivalence for invertible M.

Instances For

@[reducible, inline]

noncomputable abbrev Module.Invertible.leftCancelEquiv {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (e : TensorProduct R M N ≃ₗ[R] R) :

TensorProduct R M (TensorProduct R N P) ≃ₗ[R] P

The canonical isomorphism between a module and the result of tensoring it from the left by two mutually dual invertible modules.

Instances For

@[reducible, inline]

noncomputable abbrev Module.Invertible.rightCancelEquiv {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (e : TensorProduct R M N ≃ₗ[R] R) :

TensorProduct R (TensorProduct R P M) N ≃ₗ[R] P

The canonical isomorphism between a module and the result of tensoring it from the right by two mutually dual invertible modules.

Instances For

theorem Module.Invertible.leftCancelEquiv_comp_lTensor_comp_symm {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} {Q : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (e : TensorProduct R M N ≃ₗ[R] R) (f : P →ₗ[R] Q) :

↑(leftCancelEquiv Q e) ∘ₗ LinearMap.lTensor M (LinearMap.lTensor N f) ∘ₗ ↑(leftCancelEquiv P e).symm = f

theorem Module.Invertible.rightCancelEquiv_comp_rTensor_comp_symm {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} {Q : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (e : TensorProduct R M N ≃ₗ[R] R) (f : P →ₗ[R] Q) :

↑(rightCancelEquiv Q e) ∘ₗ LinearMap.rTensor N (LinearMap.rTensor M f) ∘ₗ ↑(rightCancelEquiv P e).symm = f

noncomputable def Module.Invertible.rTensorInv {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (e : TensorProduct R M N ≃ₗ[R] R) :

(TensorProduct R P M →ₗ[R] TensorProduct R Q M) →ₗ[R] P →ₗ[R] Q

If M is invertible, rTensorHom M admits an inverse.

Instances For

theorem Module.Invertible.rTensorInv_leftInverse {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (e : TensorProduct R M N ≃ₗ[R] R) :

Function.LeftInverse ⇑(rTensorInv P Q e) ⇑(LinearMap.rTensorHom M)

theorem Module.Invertible.rTensorInv_injective {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (e : TensorProduct R M N ≃ₗ[R] R) :

Function.Injective ⇑(rTensorInv P Q e)

noncomputable def Module.Invertible.rTensorEquiv {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (e : TensorProduct R M N ≃ₗ[R] R) :

(P →ₗ[R] Q) ≃ₗ[R] TensorProduct R P M →ₗ[R] TensorProduct R Q M

If M is an invertible R-module, (· ⊗[R] M) is an auto-equivalence of the category of R-modules.

Instances For

@[simp]

theorem Module.Invertible.rTensorEquiv_symm_apply_apply {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (e : TensorProduct R M N ≃ₗ[R] R) (a : TensorProduct R P M →ₗ[R] TensorProduct R Q M) (a✝ : P) :

((rTensorEquiv P Q e).symm a) a✝ = ((rightCancelEquiv Q e).congrRight (LinearMap.rTensor N a)) ((TensorProduct.assoc R P M N).symm (a✝ ⊗ₜ[R] e.symm 1))

@[simp]

theorem Module.Invertible.rTensorEquiv_apply_apply {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (e : TensorProduct R M N ≃ₗ[R] R) (f : P →ₗ[R] Q) (a✝ : TensorProduct R P M) :

((rTensorEquiv P Q e) f) a✝ = (TensorProduct.liftAux (TensorProduct.mk R Q M ∘ₗ f)) a✝

theorem Module.Invertible.bijective_curry {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (e : TensorProduct R M N ≃ₗ[R] R) :

Function.Bijective ⇑(TensorProduct.curry ↑e)

If there is an R-isomorphism between M ⊗[R] N and R, the induced map M → Nᵛ is an isomorphism.

noncomputable def Module.Invertible.linearEquivDual {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (e : TensorProduct R M N ≃ₗ[R] R) :

M ≃ₗ[R] Dual R N

Given M ⊗[R] N ≃ₗ[R] R, this is the induced isomorphism M ≃ₗ[R] Nᵛ.

Instances For

theorem Module.Invertible.right {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (e : TensorProduct R M N ≃ₗ[R] R) :

Module.Invertible R N

theorem Module.Invertible.left {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (e : TensorProduct R M N ≃ₗ[R] R) :

Module.Invertible R M

instance Module.Invertible.inst {R : Type u} [CommSemiring R] :

Module.Invertible R R

theorem Module.Invertible.congr {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] (e : M ≃ₗ[R] N) :

Module.Invertible R N

instance Module.Invertible.instDual (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

Module.Invertible R (Dual R M)

instance Module.Invertible.instTensorProduct (R : Type u) (M : Type v) (N : Type u_1) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] :

Module.Invertible R (TensorProduct R M N)

instance Module.Invertible.instFinite (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

Module.Finite R M

instance Module.Invertible.instProjective (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

theorem Module.Invertible.lTensor_injective_iff {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module.Invertible R M] {f : N →ₗ[R] P} :

Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f

theorem Module.Invertible.rTensor_injective_iff {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module.Invertible R M] {f : N →ₗ[R] P} :

Function.Injective ⇑(LinearMap.rTensor M f) ↔ Function.Injective ⇑f

theorem Module.Invertible.lTensor_surjective_iff {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module.Invertible R M] {f : N →ₗ[R] P} :

Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f

theorem Module.Invertible.rTensor_surjective_iff {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module.Invertible R M] {f : N →ₗ[R] P} :

Function.Surjective ⇑(LinearMap.rTensor M f) ↔ Function.Surjective ⇑f

theorem Module.Invertible.lTensor_bijective_iff {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module.Invertible R M] {f : N →ₗ[R] P} :

Function.Bijective ⇑(LinearMap.lTensor M f) ↔ Function.Bijective ⇑f

theorem Module.Invertible.rTensor_bijective_iff {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module.Invertible R M] {f : N →ₗ[R] P} :

Function.Bijective ⇑(LinearMap.rTensor M f) ↔ Function.Bijective ⇑f

theorem Module.Invertible.free_iff_linearEquiv {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

Free R M ↔ Nonempty (M ≃ₗ[R] R)

An invertible module is free iff it is isomorphic to the ring, i.e. its class is trivial in the Picard group.

theorem Module.Invertible.finrank_eq_one (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] [StrongRankCondition R] [Free R M] :

finrank R M = 1

theorem Module.Invertible.rank_eq_one (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] [StrongRankCondition R] [Free R M] :

Module.rank R M = 1

theorem Module.Invertible.toModuleEnd_bijective (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

Function.Bijective ⇑(toModuleEnd R M)

instance Module.Invertible.instFaithfulSMul (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

FaithfulSMul R M

theorem Module.Invertible.bijective_of_surjective {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f) :

Function.Bijective ⇑f

theorem Module.Invertible.rightInverse_of_leftInverse {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.LeftInverse ⇑f ⇑g) :

Function.RightInverse ⇑f ⇑g

theorem Module.Invertible.leftInverse_of_rightInverse {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.RightInverse ⇑f ⇑g) :

Function.LeftInverse ⇑f ⇑g

theorem Module.Invertible.leftInverse_iff_rightInverse {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] (f : M →ₗ[R] N) (g : N →ₗ[R] M) :

Function.LeftInverse ⇑f ⇑g ↔ Function.RightInverse ⇑f ⇑g

def Module.Invertible.linearEquivOfLeftInverse {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.LeftInverse ⇑f ⇑g) :

If f : M →ₗ[R] N and g : N →ₗ[R] M where M and N are invertible R-modules, and f is a left inverse of g, then in fact f is also the right inverse of g, and we promote this to an R-module isomorphism.

Instances For

@[simp]

theorem Module.Invertible.linearEquivOfLeftInverse_apply {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.LeftInverse ⇑f ⇑g) (x : M) :

(linearEquivOfLeftInverse hfg) x = f x

@[simp]

theorem Module.Invertible.linearEquivOfLeftInverse_symm_apply {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.LeftInverse ⇑f ⇑g) (x : N) :

(linearEquivOfLeftInverse hfg).symm x = g x

def Module.Invertible.linearEquivOfRightInverse {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.RightInverse ⇑f ⇑g) :

If f : M →ₗ[R] N and g : N →ₗ[R] M where M and N are invertible R-modules, and f is a right inverse of g, then in fact f is also the left inverse of g, and we promote this to an R-module isomorphism.

Instances For

@[simp]

theorem Module.Invertible.linearEquivOfRightInverse_apply {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.RightInverse ⇑f ⇑g) (x : M) :

(linearEquivOfRightInverse hfg) x = f x

@[simp]

theorem Module.Invertible.linearEquivOfRightInverse_symm_apply {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.RightInverse ⇑f ⇑g) (x : N) :

(linearEquivOfRightInverse hfg).symm x = g x

noncomputable def Module.Invertible.algEquivOfRing (R : Type u) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Module.Invertible R A] :

If an R-algebra A is also an invertible R-module, then it is in fact isomorphic to the base ring R. The algebra structure gives us a map A ⊗ A → A, which after tensoring by Aᵛ becomes a map A → R, which is the inverse map we seek.

Instances For

@[simp]

theorem Module.Invertible.algEquivOfRing_apply (R : Type u) {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Module.Invertible R A] (x : R) :

(algEquivOfRing R A) x = (algebraMap R A) x

instance Module.Invertible.instTensorProduct_1 (R : Type u) (M : Type v) (A : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] [CommSemiring A] [Algebra R A] :

Module.Invertible A (TensorProduct R A M)

theorem Module.Invertible.of_isLocalization {R : Type u} {M : Type v} {N : Type u_1} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Invertible R M] [CommSemiring A] [Algebra R A] (S : Submonoid R) [IsLocalization S A] (f : M →ₗ[R] N) [IsLocalizedModule S f] [Module A N] [IsScalarTower R A N] :

Module.Invertible A N

instance Module.Invertible.instLocalizationLocalizedModule (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] (S : Submonoid R) :

Module.Invertible (Localization S) (LocalizedModule S M)

instance Module.Invertible.instTensorProduct_2 (R : Type u) (M : Type v) (A : Type u_4) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] [CommSemiring A] [Algebra R A] (L : Type u_5) [AddCommMonoid L] [Module R L] [Module A L] [IsScalarTower R A L] [Module.Invertible A L] :

Module.Invertible A (TensorProduct R L M)

instance instInvertibleCarrierOutSemimoduleCatValSkeleton (R : Type u) [CommSemiring R] (M : (CategoryTheory.Skeleton (SemimoduleCat R))ˣ) :

Module.Invertible R ↑(Quotient.out ↑M)

instance instInvertibleCarrierOutModuleCatValSkeleton (R : Type u) [CommRing R] (M : (CategoryTheory.Skeleton (ModuleCat R))ˣ) :

Module.Invertible R ↑(Quotient.out ↑M)

instance instSmallUnitsSkeletonSemimoduleCat (R : Type u) [CommSemiring R] :

Small.{u, u + 1} (CategoryTheory.Skeleton (SemimoduleCat R))ˣ

instance instSmallUnitsSkeletonModuleCat (R : Type u) [CommRing R] :

Small.{u, u + 1} (CategoryTheory.Skeleton (ModuleCat R))ˣ

def CommRing.Pic (R : Type u) [CommSemiring R] :

The Picard group of a commutative semiring R consists of the invertible R-modules, up to isomorphism.

Instances For

@[implicit_reducible]

noncomputable instance instCommGroupPic (R : Type u) [CommSemiring R] :

CommGroup (CommRing.Pic R)

instance instInvertibleReprₛ (R : Type u) [CommSemiring R] (M : Type u_5) [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

Module.Invertible R (Module.Finite.reprₛ R M)

@[reducible, inline]

abbrev CommRing.Pic.AsModule {R : Type u} [CommSemiring R] (M : Pic R) :

A representative of an element in the Picard group.

Instances For

@[implicit_reducible]

noncomputable instance CommRing.Pic.instCoeSortType (R : Type u) [CommSemiring R] :

CoeSort (Pic R) (Type u)

@[implicit_reducible]

noncomputable instance CommRing.Pic.instAddCommGroupAsModule (R : Type u_7) [CommRing R] (M : Pic R) :

AddCommGroup M.AsModule

noncomputable def CommRing.Pic.mk (R : Type u) [CommSemiring R] (M : Type u_5) [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

The class of an invertible module in the Picard group.

Instances For

noncomputable def CommRing.Pic.mk.linearEquiv (R : Type u) [CommSemiring R] (M : Type u_5) [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

(Pic.mk R M).AsModule ≃ₗ[R] M

mk R M is indeed the class of M.

Instances For

theorem CommRing.Pic.mk_eq_iff {R : Type u} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] [Module.Invertible R M] {N : Pic R} :

Pic.mk R M = N ↔ Nonempty (M ≃ₗ[R] N.AsModule)

theorem CommRing.Pic.mk_eq_self {R : Type u} [CommSemiring R] {M : Pic R} :

Pic.mk R M.AsModule = M

theorem CommRing.Pic.ext_iff {R : Type u} [CommSemiring R] {M N : Pic R} :

M = N ↔ Nonempty (M.AsModule ≃ₗ[R] N.AsModule)

theorem CommRing.Pic.mk_eq_mk_iff {R : Type u} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Invertible R M] [Module.Invertible R N] :

Pic.mk R M = Pic.mk R N ↔ Nonempty (M ≃ₗ[R] N)

theorem CommRing.Pic.mk_self {R : Type u} [CommSemiring R] :

Pic.mk R R = 1

theorem CommRing.Pic.mk_eq_one_iff {R : Type u} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

Pic.mk R M = 1 ↔ Nonempty (M ≃ₗ[R] R)

theorem CommRing.Pic.mk_eq_one_iff_free {R : Type u} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

Pic.mk R M = 1 ↔ Module.Free R M

theorem CommRing.Pic.mk_eq_one (R : Type u) [CommSemiring R] (M : Type u_5) [AddCommMonoid M] [Module R M] [Module.Invertible R M] [Module.Free R M] :

Pic.mk R M = 1

instance CommRing.Pic.instFreeAsModuleOfNat {R : Type u} [CommSemiring R] :

Module.Free R (AsModule 1)

theorem CommRing.Pic.mk_tensor {R : Type u} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Module.Invertible R M] [Module.Invertible R N] :

Pic.mk R (TensorProduct R M N) = Pic.mk R M * Pic.mk R N

theorem CommRing.Pic.mk_dual {R : Type u} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] [Module.Invertible R M] :

Pic.mk R (Module.Dual R M) = (Pic.mk R M)⁻¹

theorem CommRing.Pic.inv_eq_dual {R : Type u} [CommSemiring R] (M : Pic R) :

M⁻¹ = Pic.mk R (Module.Dual R M.AsModule)

theorem CommRing.Pic.mul_eq_tensor {R : Type u} [CommSemiring R] (M N : Pic R) :

M * N = Pic.mk R (TensorProduct R M.AsModule N.AsModule)

theorem CommRing.Pic.subsingleton_iffₛ {R : Type u} [CommSemiring R] :

Subsingleton (Pic R) ↔ ∀ (M : Type u) [inst : AddCommMonoid M] [inst_1 : Module R M], Module.Invertible R M → Module.Free R M

theorem CommRing.Pic.subsingleton_iff {R : Type u} [CommRing R] :

Subsingleton (Pic R) ↔ ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module R M], Module.Invertible R M → Module.Free R M

instance CommRing.Pic.instFreeOfSubsingleton {R : Type u} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] [Module.Invertible R M] [Subsingleton (Pic R)] :

Module.Free R M

instance CommRing.Pic.instSubsingletonOfIsLocalRing (R : Type u_7) [CommRing R] [IsLocalRing R] :

Subsingleton (Pic R)

instance CommRing.Pic.instSubsingletonOfFiniteMaximalSpectrum (R : Type u_7) [CommRing R] [Finite (MaximalSpectrum R)] :

Subsingleton (Pic R)

The Picard group of a semilocal ring is trivial.

noncomputable def CommRing.Pic.mapAlgebra (R : Type u) [CommSemiring R] (A : Type u_7) [CommSemiring A] [Algebra R A] :

Pic R →* Pic A

Every R-algebra A gives rise to a homomorphism between Picard groups of R and A.

Instances For

@[simp]

theorem CommRing.Pic.mapAlgebra_apply (R : Type u) [CommSemiring R] (A : Type u_7) [CommSemiring A] [Algebra R A] (M : Pic R) :

(mapAlgebra R A) M = Pic.mk A (TensorProduct R A M.AsModule)

theorem CommRing.Pic.mapAlgebra_mapAlgebra {R : Type u} [CommSemiring R] {A : Type u_7} {B : Type u_8} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] {M : Pic R} :

(mapAlgebra A B) ((mapAlgebra R A) M) = (mapAlgebra R B) M

theorem CommRing.Pic.mapAlgebra_comp_mapAlgebra {R : Type u} [CommSemiring R] {A : Type u_7} {B : Type u_8} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] :

(mapAlgebra A B).comp (mapAlgebra R A) = mapAlgebra R B

theorem CommRing.Pic.mapAlgebra_self_apply {R : Type u} [CommSemiring R] {M : Pic R} :

(mapAlgebra R R) M = M

theorem CommRing.Pic.mapAlgebra_self {R : Type u} [CommSemiring R] :

mapAlgebra R R = MonoidHom.id (Pic R)

noncomputable def CommRing.Pic.mapRingHom {R : Type u} [CommSemiring R] {S : Type u_9} [CommSemiring S] (f : R →+* S) :

Pic R →* Pic S

Every ring homomorphism between commutative semirings induces a homomorphism between Picard groups.

Instances For

theorem CommRing.Pic.mapRingHom_algebraMap {R : Type u} [CommSemiring R] {A : Type u_7} [CommSemiring A] [Algebra R A] :

mapRingHom (algebraMap R A) = mapAlgebra R A

theorem CommRing.Pic.mapRingHom_comp_mapRingHom {R : Type u} [CommSemiring R] {S : Type u_9} {T : Type u_10} [CommSemiring S] [CommSemiring T] {f : R →+* S} {g : S →+* T} :

(mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)

theorem CommRing.Pic.mapRingHom_mapRingHom {R : Type u} [CommSemiring R] {S : Type u_9} {T : Type u_10} [CommSemiring S] [CommSemiring T] {f : R →+* S} {g : S →+* T} {M : Pic R} :

(mapRingHom g) ((mapRingHom f) M) = (mapRingHom (g.comp f)) M

theorem CommRing.Pic.mapRingHom_id {R : Type u} [CommSemiring R] :

mapRingHom (RingHom.id R) = MonoidHom.id (Pic R)

theorem CommRing.Pic.mapRingHom_id_apply {R : Type u} [CommSemiring R] {M : Pic R} :

(mapRingHom (RingHom.id R)) M = M

noncomputable def CommRing.Pic.functor :

CategoryTheory.Functor CommSemiRingCat CommGrpCat

Picard group as a functor from the category of commutative semirings to the category of abelian groups.

Instances For

noncomputable def CommRing.relPic (R : Type u) [CommSemiring R] (A : Type u_7) [CommSemiring A] [Algebra R A] :

Subgroup (Pic R)

The relative Picard group of an R-algebra A, denoted Pic(A/R), defined to be the kernel of Pic.mapAlgebra R A.

Instances For

theorem CommRing.relPic_eq_top (R : Type u) [CommSemiring R] (A : Type u_7) [CommSemiring A] [Algebra R A] [Subsingleton (Pic A)] :

relPic R A = ⊤

theorem Module.Invertible.tensorProductComm_eq_refl (R : Type u_5) (M : Type u_6) [CommRing R] [AddCommGroup M] [Module R M] [Module.Invertible R M] :

TensorProduct.comm R M M = LinearEquiv.refl R (TensorProduct R M M)

theorem Module.Invertible.tmul_comm {R : Type u_5} {M : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [Module.Invertible R M] {m₁ m₂ : M} :

m₁ ⊗ₜ[R] m₂ = m₂ ⊗ₜ[R] m₁

instance Submodule.projective_units {R : Type u} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] (I : (Submodule R A)ˣ) :

Module.Projective R ↥↑I

theorem Submodule.projective_of_isUnit {R : Type u} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] {I : Submodule R A} (hI : IsUnit I) :

Module.Projective R ↥I

noncomputable def Submodule.tensorEquivMul {R : Type u} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] (I J : (Submodule R A)ˣ) :

TensorProduct R ↥↑I ↥↑J ≃ₗ[R] ↥↑(I * J)

Given two invertible R-submodules in an R-algebra A, the R-linear map from I ⊗[R] J to I * J induced by multiplication is an isomorphism.

Instances For

noncomputable def Submodule.tensorInvEquiv {R : Type u} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] (I : (Submodule R A)ˣ) :

TensorProduct R ↥↑I ↥↑I⁻¹ ≃ₗ[R] R

Given an invertible R-submodule I in an R-algebra A, the R-linear map from I ⊗[R] I⁻¹ to R induced by multiplication is an isomorphism.

Instances For

instance Submodule.instInvertibleSubtypeMemVal {R : Type u} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] (I : (Submodule R A)ˣ) :

Module.Invertible R ↥↑I

noncomputable def Submodule.unitsToPic (R : Type u) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] :

(Submodule R A)ˣ →* CommRing.Pic R

The group homomorphism from the invertible submodules in a faithful algebra over R to the Picard group of R. See Lemma 2.2 in [RobertsSingh1993].

Instances For

@[simp]

theorem Submodule.unitsToPic_apply (R : Type u) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] (I : (Submodule R A)ˣ) :

(unitsToPic R A) I = CommRing.Pic.mk R ↥↑I

noncomputable def Submodule.unitsToPicEquiv {R : Type u} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] (I : (Submodule R A)ˣ) :

((unitsToPic R A) I).AsModule ≃ₗ[R] ↥↑I

The image of an invertible R-submodule I ⊆ A under unitsToPic is isomorphic to I.

Instances For

theorem Submodule.ker_unitsToPic (R : Type u) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] :

(unitsToPic R A).ker = (Units.map ↑(spanSingleton R)).range

theorem Submodule.mulExact_unitsMap_spanSingleton_unitsToPic (R : Type u) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] :

Function.MulExact ⇑(Units.map ↑(spanSingleton R)) ⇑(unitsToPic R A)

Exactness of the sequence 1 → Rˣ → Aˣ → (Submodule R A)ˣ → Pic R → Pic A at (Submodule R A)ˣ.

noncomputable def Module.Flat.toAlgebra {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) :

If a flat R-module becomes free of rank 1 after base-changing to a faithful R-algebra A, then it embeds into A.

Instances For

theorem Module.Flat.toAlgebra_injective {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Flat R M] [FaithfulSMul R A] :

Function.Injective ⇑(toAlgebra e)

@[reducible, inline]

noncomputable abbrev Module.Flat.submoduleAlgebra {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) :

A flat R-module as a R-submodule of a faithful R-algebra.

Instances For

noncomputable def Module.Flat.submoduleAlgebraEquiv {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Flat R M] [FaithfulSMul R A] :

↥(submoduleAlgebra e) ≃ₗ[R] M

An isomorphism between a flat R-module and its realization as a submodule in a faithful R-algebra.

Instances For

instance Module.Flat.instSubtypeMemSubmoduleSubmoduleAlgebra {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Flat R M] [FaithfulSMul R A] :

Flat R ↥(submoduleAlgebra e)

instance Module.Flat.instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Flat R M] [FaithfulSMul R A] [Module.Invertible R M] :

Module.Invertible R ↥(submoduleAlgebra e)

noncomputable def Module.Flat.tensorSubmoduleAlgebraEquiv {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Flat R M] [FaithfulSMul R A] :

TensorProduct R A ↥(submoduleAlgebra e) ≃ₗ[A] A

When a flat R-module M is embedded as a submodule of a faithful R-algebra A, the multiplication map induces an isomorphism A ⊗[R] M ≃ₗ[A] A.

Instances For

theorem Module.Flat.top_mul_submoduleAlgebra {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Flat R M] [FaithfulSMul R A] :

⊤ * submoduleAlgebra e = ⊤

noncomputable def Module.Flat.tensorSubmoduleAlgebraEquivMul {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Flat R M] [FaithfulSMul R A] (I : Submodule R A) :

TensorProduct R ↥I ↥(submoduleAlgebra e) ≃ₗ[R] ↥(I * submoduleAlgebra e)

When a flat R-module M is embedded as a submodule of a faithful R-algebra A, we have I ⊗[R] M ≃ₗ[R] I * M for any R-submodule I of A.

Instances For

@[deprecated Module.Flat.toAlgebra (since := "2025-11-23")]

def Module.Invertible.embAlgebra {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) :

Alias of Module.Flat.toAlgebra.

If a flat R-module becomes free of rank 1 after base-changing to a faithful R-algebra A, then it embeds into A.

Instances For

@[deprecated Module.Flat.toAlgebra_injective (since := "2025-11-23")]

theorem Module.Invertible.embAlgebra_injective {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Flat R M] [FaithfulSMul R A] :

Function.Injective ⇑(Flat.toAlgebra e)

Alias of Module.Flat.toAlgebra_injective.

@[deprecated Module.Flat.submoduleAlgebra (since := "2025-11-23")]

def Module.Invertible.toSubmodule {R : Type u} {M : Type v} {A : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring A] [Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) :

Alias of Module.Flat.submoduleAlgebra.

A flat R-module as a R-submodule of a faithful R-algebra.

Instances For

theorem Submodule.range_unitsToPic (R : Type u) (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [FaithfulSMul R A] :

(unitsToPic R A).range = CommRing.relPic R A

theorem Submodule.mulExact_unitsToPic_mapAlgebra (R : Type u) (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [FaithfulSMul R A] :

Function.MulExact ⇑(unitsToPic R A) ⇑(CommRing.Pic.mapAlgebra R A)

Exactness of the sequence 1 → Rˣ → Aˣ → (Submodule R A)ˣ → Pic R → Pic A at Pic R.

noncomputable def Submodule.unitsQuotEquivRelPic (R : Type u) (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [FaithfulSMul R A] :

(Submodule R A)ˣ ⧸ (Units.map ↑(spanSingleton R)).range ≃* ↥(CommRing.relPic R A)

If A is a faithful R-algebra, the relative Picard group Pic(A/R) is isomorphic to the group of the invertible R-submodules in A modulo the principal submodules.

Instances For

@[simp]

theorem Submodule.unitsQuotEquivRelPic_symm_apply (R : Type u) (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [FaithfulSMul R A] (a✝ : ↥(CommRing.relPic R A)) :

(unitsQuotEquivRelPic R A).symm a✝ = (QuotientGroup.congr (unitsToPic R A).ker (Units.map ↑(spanSingleton R)).range (MulEquiv.refl (Submodule R A)ˣ) ⋯) ((QuotientGroup.quotientKerEquivRange (unitsToPic R A)).symm ((MulEquiv.subgroupCongr ⋯).symm a✝))

@[simp]

theorem Submodule.unitsQuotEquivRelPic_apply_coe (R : Type u) (A : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [FaithfulSMul R A] (a✝ : (Submodule R A)ˣ ⧸ (Units.map ↑(spanSingleton R)).range) :

↑((unitsQuotEquivRelPic R A) a✝) = ↑((QuotientGroup.quotientKerEquivRange (unitsToPic R A)) ((QuotientGroup.congr (Units.map ↑(spanSingleton R)).range (unitsToPic R A).ker (MulEquiv.refl (Submodule R A)ˣ) ⋯) a✝))

noncomputable def ClassGroup.equivPic (R : Type u_5) [CommRing R] [IsDomain R] :

ClassGroup R ≃* CommRing.Pic R

The class group of a domain is isomorphic to the Picard group.

Instances For

@[simp]

theorem ClassGroup.equivPic_symm_apply (R : Type u_5) [CommRing R] [IsDomain R] (a✝ : CommRing.Pic R) :

(equivPic R).symm a✝ = (mulEquivUnitsSubmoduleQuotRange R).symm ((QuotientGroup.congr (Submodule.unitsToPic R (FractionRing R)).ker (Units.map ↑(Submodule.spanSingleton R)).range (MulEquiv.refl (Submodule R (FractionRing R))ˣ) ⋯) ((QuotientGroup.quotientKerEquivRange (Submodule.unitsToPic R (FractionRing R))).symm ((MulEquiv.subgroupCongr ⋯).symm ((MulEquiv.subgroupCongr ⋯).symm (Subgroup.topEquiv.symm a✝)))))

@[simp]

theorem ClassGroup.equivPic_apply (R : Type u_5) [CommRing R] [IsDomain R] (a✝ : ClassGroup R) :

(equivPic R) a✝ = ↑((QuotientGroup.quotientKerEquivRange (Submodule.unitsToPic R (FractionRing R))) ((QuotientGroup.congr (Units.map ↑(Submodule.spanSingleton R)).range (Submodule.unitsToPic R (FractionRing R)).ker (MulEquiv.refl (Submodule R (FractionRing R))ˣ) ⋯) ((mulEquivUnitsSubmoduleQuotRange R) a✝)))

instance instSubsingletonPicOfIsDomainOfNonemptyNormalizedGCDMonoid (R : Type u_5) [CommRing R] [IsDomain R] [Nonempty (NormalizedGCDMonoid R)] :

Subsingleton (CommRing.Pic R)

The Picard group of a domain with normalizable gcd is trivial. This includes unique factorization domains.

theorem Module.Invertible.exists_linearEquiv_ideal (R : Type u_5) (M : Type u_6) [CommRing R] [AddCommGroup M] [Module R M] [Module.Invertible R M] [Subsingleton (CommRing.Pic (FractionRing R))] :

∃ (I : Ideal R), Nonempty (M ≃ₗ[R] ↥I)

If FractionRing R has trivial Picard group, every invertible R-module is isomorphic to an ideal.

theorem Ideal.eq_top_of_mk_tensor_eq_one {R : Type u_5} [CommRing R] [IsFractionRing R R] (I J : Ideal R) [Module.Invertible R ↥I] [Module.Invertible R ↥J] (h : CommRing.Pic.mk R (TensorProduct R ↥I ↥J) = 1) :

I = ⊤ ∧ J = ⊤

In a total ring of fractions, if two ideals are inverse to each other in the Picard group, the only possibility is that they are both the whole ring.