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.

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.

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, Proposition 3.5.
• Stacks: Picard groups of rings

TODO

Show:

• The Picard group of a commutative domain is isomorphic to its ideal class group.

• All commutative semi-local rings, in particular Artinian rings, have trivial Picard group.

• All unique factorization domains have trivial Picard group.

• 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] : Prop

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)

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.

Equations

• Module.Invertible.linearEquiv R M = LinearEquiv.ofBijective (contractLeft R M) ⋯

@[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.

Equations

• Module.Invertible.leftCancelEquiv P e = ((TensorProduct.assoc R M N P).symm.trans (LinearEquiv.rTensor P e)).trans (TensorProduct.lid R P)

@[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.

Equations

• Module.Invertible.rightCancelEquiv P e = ((TensorProduct.assoc R P M N).trans (LinearEquiv.lTensor P e)).trans (TensorProduct.rid R P)

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Module.Invertible.rTensorEquiv P Q e = { toLinearMap := LinearMap.rTensorHom M, invFun := ⇑(Module.Invertible.rTensorInv P Q e), left_inv := ⋯, right_inv := ⋯ }

@[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ᵛ.

Equations

• Module.Invertible.linearEquivDual e = LinearEquiv.ofBijective (TensorProduct.curry ↑e) ⋯

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] : Projective 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) : M ≃ₗ[R] N

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.

Equations

• Module.Invertible.linearEquivOfLeftInverse hfg = LinearEquiv.ofLinear f g ⋯ ⋯

@[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) : M ≃ₗ[R] N

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.

Equations

• Module.Invertible.linearEquivOfRightInverse hfg = LinearEquiv.ofLinear f g ⋯ ⋯

@[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) [CommSemiring R] (A : Type u_5) [Semiring A] [Algebra R A] [Module.Invertible R A] : R ≃ₐ[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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.Invertible.algEquivOfRing_apply (R : Type u) [CommSemiring R] {A : Type u_5} [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] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module R M] [Module.Invertible R M] : 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] [CommSemiring A] [AddCommMonoid M] [AddCommMonoid N] [Algebra R A] [Module R M] [Module R N] [Module.Invertible R M] (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.instTensorProduct_2 (R : Type u) (M : Type v) (A : Type u_4) [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module R M] [Module.Invertible R M] (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)

noncomputable def Module.Invertible.embAlgebra (R : Type u) (M : Type v) (A : Type u_4) [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module R M] [Module.Invertible R M] [Free A (TensorProduct R A M)] : M →ₗ[R] A

An invertible R-module embeds into an R-algebra that R injects into, provided A ⊗[R] M is a free A-module.

Equations

• Module.Invertible.embAlgebra R M A = ↑(LinearEquiv.restrictScalars R ⋯.some) ∘ₗ LinearMap.rTensor M (Algebra.ofId R A).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm

theorem Module.Invertible.embAlgebra_injective (R : Type u) (M : Type v) (A : Type u_4) [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module R M] [Module.Invertible R M] [FaithfulSMul R A] [Free A (TensorProduct R A M)] : Function.Injective ⇑(embAlgebra R M A)

noncomputable def Module.Invertible.toSubmodule (R : Type u) (M : Type v) (A : Type u_4) [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module R M] [Module.Invertible R M] [Free A (TensorProduct R A M)] : Submodule R A

An invertible R-module as a R-submodule of an R-algebra.

Equations

• Module.Invertible.toSubmodule R M A = LinearMap.range (Module.Invertible.embAlgebra R M A)

instance instInvertibleCarrierOutModuleCatValSkeleton (R : Type u) [CommRing R] (M : (CategoryTheory.Skeleton (ModuleCat R))ˣ) : Module.Invertible R ↑(Quotient.out ↑M)

instance instSmallUnitsSkeletonModuleCat (R : Type u) [CommRing R] : Small.{u, u + 1} (CategoryTheory.Skeleton (ModuleCat R))ˣ

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

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

Equations

• CommRing.Pic R = Shrink.{?u.10, ?u.10 + 1} (CategoryTheory.Skeleton (ModuleCat R))ˣ

noncomputable instance instCommGroupPic (R : Type u) [CommRing R] : CommGroup (CommRing.Pic R)

Equations

• instCommGroupPic R = (equivShrink (CategoryTheory.Skeleton (ModuleCat R))ˣ).symm.commGroup

instance instInvertibleRepr (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup 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} [CommRing R] (M : Pic R) : Type u

A representative of an element in the Picard group.

Equations

• M.AsModule = ↑(Quotient.out ↑((equivShrink (CategoryTheory.Skeleton (ModuleCat R))ˣ).symm M))

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

Equations

• CommRing.Pic.instCoeSortType R = { coe := CommRing.Pic.AsModule }

noncomputable def CommRing.Pic.mk (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Invertible R M] : Pic R

The class of an invertible module in the Picard group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommRing.Pic.mk.linearEquiv (R : Type u) [CommRing R] (M : Type u_1) [AddCommGroup M] [Module R M] [Module.Invertible R M] : (Pic.mk R M).AsModule ≃ₗ[R] M

mk R M is indeed the class of M.

Equations

• One or more equations did not get rendered due to their size.

theorem CommRing.Pic.mk_eq_iff {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup 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} [CommRing R] {M : Pic R} : Pic.mk R M.AsModule = M

theorem CommRing.Pic.ext_iff {R : Type u} [CommRing R] {M N : Pic R} : M = N ↔ Nonempty (M.AsModule ≃ₗ[R] N.AsModule)

theorem CommRing.Pic.mk_eq_mk_iff {R : Type u} [CommRing R] {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup 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} [CommRing R] : Pic.mk R R = 1

theorem CommRing.Pic.mk_eq_one_iff {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] [Module.Invertible R M] : Pic.mk R M = 1 ↔ Nonempty (M ≃ₗ[R] R)

theorem CommRing.Pic.mk_eq_one {R : Type u} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] [Module.Invertible R M] [Module.Free R M] : Pic.mk R M = 1

theorem CommRing.Pic.mk_tensor {R : Type u} [CommRing R] {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup 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} [CommRing R] {M : Type u_1} [AddCommGroup 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} [CommRing R] (M : Pic R) : M⁻¹ = Pic.mk R (Module.Dual R M.AsModule)

theorem CommRing.Pic.mul_eq_tensor {R : Type u} [CommRing R] (M N : Pic R) : M * N = Pic.mk R (TensorProduct R M.AsModule N.AsModule)

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} [CommRing R] {M : Type u_1} [AddCommGroup M] [Module R M] [Module.Invertible R M] [Subsingleton (Pic R)] : Module.Free R M

instance CommRing.Pic.instSubsingletonOfIsLocalRing {R : Type u} [CommRing R] [IsLocalRing R] : Subsingleton (Pic R)

instance Submodule.projective_unit {R : Type u_1} {A : Type u_2} [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_1} {A : Type u_2} [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_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] [FaithfulSMul R A] (S : Submonoid R) [IsLocalization S 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.

Equations

• Submodule.tensorEquivMul S I J = LinearEquiv.ofBijective ((↑I).mulMap' ↑J) ⋯

noncomputable def Submodule.tensorInvEquiv {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] [FaithfulSMul R A] (S : Submonoid R) [IsLocalization S 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.

Equations

• One or more equations did not get rendered due to their size.

theorem Units.submodule_invertible {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] [FaithfulSMul R A] (S : Submonoid R) [IsLocalization S A] (I : (Submodule R A)ˣ) : Module.Invertible R ↥↑I

noncomputable def Submodule.unitsToPic (R : Type u_3) (A : Type u_4) [CommRing R] [CommRing A] [Algebra R A] [FaithfulSMul R A] (S : Submonoid R) [IsLocalization S A] : (Submodule R A)ˣ →* CommRing.Pic R

The group homomorphism from the invertible submodules in a localization of R to the Picard group of R.

Equations

• Submodule.unitsToPic R A S = { toFun := fun (I : (Submodule R A)ˣ) => CommRing.Pic.mk R ↥↑I, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Submodule.unitsToPic_apply (R : Type u_3) (A : Type u_4) [CommRing R] [CommRing A] [Algebra R A] [FaithfulSMul R A] (S : Submonoid R) [IsLocalization S A] (I : (Submodule R A)ˣ) : (unitsToPic R A S) I = CommRing.Pic.mk R ↥↑I