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 [Rob93] or Exercise I.3.7(iv) and Proposition I.3.5 in [Wei13].

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
• [Wei13], https://sites.math.rutgers.edu/~weibel/Kbook/Kbook.I.pdf
• Stacks: Picard groups of rings

TODO

Show:

• 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) (A : Type u_4) [CommSemiring R] [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) {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] : Type u

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

Equations

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

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

Equations

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

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) : Type u

A representative of an element in the Picard group.

Equations

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

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

Equations

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

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

Equations

• CommRing.Pic.instAddCommGroupAsModule R M = Module.addCommMonoidToAddCommGroup R

noncomputable def CommRing.Pic.mk (R : Type u) [CommSemiring R] (M : Type u_5) [AddCommMonoid 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) [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.

Equations

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

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.

Equations

• CommRing.Pic.mapAlgebra R A = { toFun := fun (M : CommRing.Pic R) => CommRing.Pic.mk A (TensorProduct R A M.AsModule), map_one' := ⋯, map_mul' := ⋯ }

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

Equations

• CommRing.Pic.mapRingHom f = CommRing.Pic.mapAlgebra R S

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.

Equations

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

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.

Equations

• CommRing.relPic R A = (CommRing.Pic.mapAlgebra R A).ker

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.

Equations

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

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.

Equations

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

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 [Rob93].

Equations

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

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

Equations

• Submodule.unitsToPicEquiv I = ⋯.some.symm

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) : M →ₗ[R] 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.

Equations

• Module.Flat.toAlgebra e = ↑(LinearEquiv.restrictScalars R e) ∘ₗ LinearMap.rTensor M (Algebra.ofId R A).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm

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) : Submodule R A

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

Equations

• Module.Flat.submoduleAlgebra e = (Module.Flat.toAlgebra e).range

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.

Equations

• Module.Flat.submoduleAlgebraEquiv e = (LinearEquiv.ofInjective (Module.Flat.toAlgebra e) ⋯).symm

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.

Equations

• Module.Flat.tensorSubmoduleAlgebraEquiv e = LinearEquiv.ofBijective (LinearMap.mul'' R A ∘ₗ (TensorProduct.AlgebraTensorModule.lTensor A A) (Module.Flat.submoduleAlgebra e).subtype) ⋯

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.

Equations

• Module.Flat.tensorSubmoduleAlgebraEquivMul e I = LinearEquiv.ofBijective (I.mulMap' (Module.Flat.submoduleAlgebra e)) ⋯

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

Equations

• @Module.Invertible.embAlgebra = @Module.Flat.toAlgebra

@[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) : Submodule R A

Alias of Module.Flat.submoduleAlgebra.

---

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

Equations

• @Module.Invertible.toSubmodule = @Module.Flat.submoduleAlgebra

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.

Equations

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

@[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✝))

@[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✝))

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.

Equations

• ClassGroup.equivPic R = (ClassGroup.mulEquivUnitsSubmoduleQuotRange R).trans ((Submodule.unitsQuotEquivRelPic R (FractionRing R)).trans ((MulEquiv.subgroupCongr ⋯).trans Subgroup.topEquiv))

@[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✝)))

@[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✝)))))

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.