Class group map induced by an extension of domains

For an injective ring homomorphism f : A →+* B of commutative domains, we construct the group homomorphism ClassGroup.map f hf : ClassGroup A →* ClassGroup B given by pushing fractional ideals forward along f. For an injective extension A → B (equivalently Module.IsTorsionFree A B), ClassGroup.extendedHom A B is the special case of the algebra map.

Main definitions

• ClassGroup.map f hf: the map between class groups induced by an injective ring homomorphism.
• ClassGroup.mulEquiv g: the isomorphism between class groups induced by a ring isomorphism.
• ClassGroup.extendedHom A B: the induced map between the class groups.
• ClassGroup.extendedIdeal A B: the extension of a nonzero integral ideal.

Main results

• ClassGroup.map_mk0: compatibility of ClassGroup.map with nonzero integral ideals.
• ClassGroup.map_id, ClassGroup.map_map: functoriality of ClassGroup.map.
• ClassGroup.extendedHom_mk: compatibility with representatives as fractional ideals.
• ClassGroup.extendedHom_mk0: compatibility with representatives as nonzero integral ideals.
• ClassGroup.extendedHom_comp: compatibility of extension in a tower A → B → C.
• ClassGroup.extendedHom_eq_one_of_forall_isPrincipal: if the extension of every ideal is principal, then ClassGroup.extendedHom A B is trivial.

noncomputable def ClassGroup.map {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] (f : A →+* B) (hf : Function.Injective ⇑f) : ClassGroup A →* ClassGroup B

The monoid homomorphism ClassGroup A → ClassGroup B induced by an injective ring homomorphism f : A →+* B of domains, given by extending fractional ideals along f.

Equations

• ClassGroup.map f hf = QuotientGroup.map (toPrincipalIdeal A (FractionRing A)).range (toPrincipalIdeal B (FractionRing B)).range (Units.map ↑(FractionalIdeal.extendedHom' (FractionRing B) ⋯)) ⋯

@[simp]

theorem ClassGroup.map_quotientMk {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] (f : A →+* B) (hf : Function.Injective ⇑f) (α : (FractionalIdeal (nonZeroDivisors A) (FractionRing A))ˣ) : (map f hf) ↑α = ↑((Units.map ↑(FractionalIdeal.extendedHom' (FractionRing B) ⋯)) α)

@[simp]

theorem ClassGroup.map_id {A : Type u_1} [CommRing A] [IsDomain A] (x : ClassGroup A) : (map (RingHom.id A) ⋯) x = x

theorem ClassGroup.map_map {A : Type u_1} {B : Type u_2} {C : Type u_3} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] [CommRing C] [IsDomain C] (f : A →+* B) (hf : Function.Injective ⇑f) (g : B →+* C) (hg : Function.Injective ⇑g) (x : ClassGroup A) : (map g hg) ((map f hf) x) = (map (g.comp f) ⋯) x

theorem ClassGroup.map_mk0 {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [IsDedekindDomain A] [IsDedekindDomain B] (f : A →+* B) (hf : Function.Injective ⇑f) (I : ↥(nonZeroDivisors (Ideal A))) : (map f hf) (mk0 I) = mk0 ⟨Ideal.map f ↑I, ⋯⟩

noncomputable def ClassGroup.mulEquiv {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] (g : A ≃+* B) : ClassGroup A ≃* ClassGroup B

A ring isomorphism A ≃+* B induces an isomorphism on their class groups.

Equations

• ClassGroup.mulEquiv g = { toFun := ⇑(ClassGroup.map ↑g ⋯), invFun := ⇑(ClassGroup.map ↑g.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem ClassGroup.mulEquiv_apply {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] (g : A ≃+* B) (a : ClassGroup A) : (mulEquiv g) a = (map ↑g ⋯) a

@[simp]

theorem ClassGroup.mulEquiv_symm_apply {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] (g : A ≃+* B) (a : ClassGroup B) : (mulEquiv g).symm a = (map ↑g.symm ⋯) a

theorem ClassGroup.mulEquiv_mk0 {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [IsDedekindDomain A] [IsDedekindDomain B] (g : A ≃+* B) (I : ↥(nonZeroDivisors (Ideal A))) : (mulEquiv g) (mk0 I) = mk0 ⟨Ideal.map g ↑I, ⋯⟩

noncomputable def ClassGroup.extendedHom (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDomain A] [IsDomain B] : ClassGroup A →* ClassGroup B

The monoid homomorphism ClassGroup A → ClassGroup B induced by an injective extension of domains A → B.

Equations

• ClassGroup.extendedHom A B = ClassGroup.map (algebraMap A B) ⋯

@[simp]

theorem ClassGroup.extendedHom_quotientMk (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDomain A] [IsDomain B] (α : (FractionalIdeal (nonZeroDivisors A) (FractionRing A))ˣ) : (extendedHom A B) ↑α = ↑((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) α)

@[simp]

theorem ClassGroup.extendedHom_mk (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDomain A] [IsDomain B] (I : (FractionalIdeal (nonZeroDivisors A) (FractionRing A))ˣ) : (extendedHom A B) ((mk (FractionRing A)) I) = (mk (FractionRing B)) ((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) I)

@[reducible, inline]

abbrev ClassGroup.extendedIdeal (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDomain A] [IsDomain B] (I : ↥(nonZeroDivisors (Ideal A))) : ↥(nonZeroDivisors (Ideal B))

The extension of a nonzero integral ideal along an injective extension of domains.

Equations

• ClassGroup.extendedIdeal A B I = ⟨Ideal.map (algebraMap A B) ↑I, ⋯⟩

@[simp]

theorem ClassGroup.extendedIdeal_extendedIdeal (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDomain A] [IsDomain B] (C : Type u_3) [CommRing C] [IsDomain C] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [Module.IsTorsionFree B C] [Module.IsTorsionFree A C] (I : ↥(nonZeroDivisors (Ideal A))) : extendedIdeal B C (extendedIdeal A B I) = extendedIdeal A C I

theorem ClassGroup.extendedHom_mk0' (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDedekindDomain A] [IsDomain B] (I : ↥(nonZeroDivisors (Ideal A))) : (extendedHom A B) (mk0 I) = (mk (FractionRing B)) ((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) ((FractionalIdeal.mk0 (FractionRing A)) I))

theorem ClassGroup.extendedHom_mk0 (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDedekindDomain A] [IsDedekindDomain B] (I : ↥(nonZeroDivisors (Ideal A))) : (extendedHom A B) (mk0 I) = mk0 (extendedIdeal A B I)

@[simp]

theorem ClassGroup.extendedHom_comp_apply (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDedekindDomain A] (C : Type u_3) [CommRing C] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [Module.IsTorsionFree B C] [Module.IsTorsionFree A C] [IsDedekindDomain C] [IsDedekindDomain B] (x : ClassGroup A) : (extendedHom B C) ((extendedHom A B) x) = (extendedHom A C) x

theorem ClassGroup.extendedHom_comp (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDedekindDomain A] (C : Type u_3) [CommRing C] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [Module.IsTorsionFree B C] [Module.IsTorsionFree A C] [IsDedekindDomain C] [IsDedekindDomain B] : (extendedHom B C).comp (extendedHom A B) = extendedHom A C

theorem ClassGroup.extendedHom_eq_one_of_forall_isPrincipal (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] [Module.IsTorsionFree A B] [IsDedekindDomain A] [IsDedekindDomain B] (h : ∀ (I : Ideal A), Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)) : extendedHom A B = 1