Class group map induced by an extension of domains

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

Main definitions

• 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.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.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

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

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