def CartierDivisorGroup (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : Type u_2

The Cartier divisor group of a Dedekind domain A with fraction field K, defined algebraically as the units in the monoid of fractional ideals (cf. Def 30, Lec 14).

@[implicit_reducible]

noncomputable instance CartierDivisorGroup.instCommGroup (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : CommGroup (CartierDivisorGroup A K)

The Cartier divisor group is a commutative group, inherited from the units of fractional ideals.

@[implicit_reducible]

noncomputable instance CartierDivisorGroup.instInhabited (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : Inhabited (CartierDivisorGroup A K)

The Cartier divisor group is inhabited by the trivial divisor 1.

noncomputable def CartierDivisorGroup.equiv (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : CartierDivisorGroup A K ≃* (FractionalIdeal (nonZeroDivisors A) K)ˣ

The tautological multiplicative equivalence between CartierDivisorGroup A K and the units of fractional ideals.

noncomputable def CartierDivisorGroup.toUnits (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (D : CartierDivisorGroup A K) : (FractionalIdeal (nonZeroDivisors A) K)ˣ

Forget the Cartier divisor wrapping to obtain the underlying unit fractional ideal.

noncomputable def CartierDivisorGroup.toFractionalIdeal (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (D : CartierDivisorGroup A K) : FractionalIdeal (nonZeroDivisors A) K

View a Cartier divisor as the underlying fractional ideal (forgetting invertibility).

noncomputable def CartierDivisorGroup.principalDivisor (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : Kˣ →* CartierDivisorGroup A K

The principal divisor map Kˣ → CartierDivisorGroup A K sending a unit x to the divisor of the principal fractional ideal (x).

noncomputable def CartierDivisorGroup.picardEquiv (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : ClassGroup A ≃* CartierDivisorGroup A K ⧸ (principalDivisor A K).range

The Picard group of a Dedekind domain is the quotient of the Cartier divisor group by the subgroup of principal divisors; this realises it as the ideal class group.

theorem CartierDivisorGroup.isPrincipal_iff (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (D : CartierDivisorGroup A K) : D ∈ (principalDivisor A K).range ↔ ∃ (x : K), FractionalIdeal.spanSingleton (nonZeroDivisors A) x = toFractionalIdeal A K D

A Cartier divisor is principal iff its underlying fractional ideal is generated by a single element of K.

theorem CartierDivisorGroup.linearlyEquivalent_iff (A : Type u_1) [CommRing A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (D₁ D₂ : CartierDivisorGroup A K) : (QuotientGroup.mk' (principalDivisor A K).range) D₁ = (QuotientGroup.mk' (principalDivisor A K).range) D₂ ↔ ∃ (x : Kˣ), D₁ * (principalDivisor A K) x = D₂

Two Cartier divisors are linearly equivalent (i.e. equal in the Picard group) iff they differ by a principal divisor.

noncomputable def CartierDivisorGroup.fromIdeal (A : Type u_1) [CommRing A] [IsDomain A] [IsDedekindDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] : ↥(nonZeroDivisors (Ideal A)) →* CartierDivisorGroup A K

Promote a nonzero ordinary ideal of A to a Cartier divisor by viewing it as a fractional ideal of K.