@[reducible, inline]

abbrev Prop22.DivC (R : Type u_1) [CommRing R] : Type u_1

Cartier divisors on the affine scheme Spec R realised as units of the fractional ideals in the fraction field.

@[reducible, inline]

noncomputable abbrev Prop22.principalHom (R : Type u_1) [CommRing R] [IsDomain R] : (FractionRing R)ˣ →* DivC R

The principal-Cartier-divisor homomorphism: a nonzero element of the fraction field maps to its principal fractional ideal.

noncomputable def Prop22.cartierToPicHom (R : Type u_1) [CommRing R] [IsDomain R] : DivC R →* CommRing.Pic R

The Cartier-to-Picard homomorphism DivC(R) → Pic(R), sending a Cartier divisor to its associated line bundle.

theorem Prop22.cartier_to_pic_surjective (R : Type u_1) [CommRing R] [IsDomain R] : Function.Surjective ⇑(cartierToPicHom R)

The map from Cartier divisors to the Picard group is surjective: every line bundle arises from a Cartier divisor.

theorem Prop22.ker_cartier_to_pic (R : Type u_1) [CommRing R] [IsDomain R] : (cartierToPicHom R).ker = (principalHom R).range

The kernel of the Cartier-to-Picard homomorphism is exactly the image of the principal-divisor map: Pic(R) = DivC / principals.

noncomputable def prop22_cartier_divisors_iso_line_bundles (R : Type u_1) [CommRing R] [IsDomain R] : ClassGroup R ≃* CommRing.Pic R

Proposition 22: the class group of Cartier divisors is isomorphic to the Picard group of line bundles, ClassGroup R ≃* Pic R.

theorem prop22_picard_iso_classGroup (R : Type u_1) [CommRing R] [IsDomain R] : Nonempty (ClassGroup R ≃* CommRing.Pic R)

Proposition 22 (existence): there is an isomorphism ClassGroup R ≃* Pic R.

theorem prop22_picard_iso_cartier_quotient_geometric (R : Type u_1) [CommRing R] [IsDomain R] [IsDedekindDomain R] : Nonempty (ClassGroup R ≃* CommRing.Pic R)

Proposition 22 over Dedekind domains: ClassGroup R ≃* Pic R, expressing the Picard group as Cartier divisors modulo principal divisors.