Invariance of Ulm data under isomorphism

This module contains the easy direction of Ulm's theorem: isomorphisms preserve both the Ulm filtration and the classical P_α / P_{α+1} quotients, hence the Ulm invariants.

theorem UlmsTheorem.ulmSubgroup_map_iso (p : ℕ) {G H : Type u} [AddCommGroup G] [AddCommGroup H] (φ : G ≃+ H) (α : Ordinal.{u_1}) : AddSubgroup.map φ.toAddMonoidHom (ulmSubgroup p α) = ulmSubgroup p α

An isomorphism of abelian groups preserves the Ulm subgroups.

theorem UlmsTheorem.pSocleAt_map_iso (p : ℕ) {G H : Type u} [AddCommGroup G] [AddCommGroup H] (φ : G ≃+ H) (α : Ordinal.{u_1}) : AddSubgroup.map φ.toAddMonoidHom (pSocleAt p α) = pSocleAt p α

An isomorphism preserves the filtered p-socle layers P_α.

noncomputable def UlmsTheorem.pSocleAtIso (p : ℕ) {G H : Type u} [AddCommGroup G] [AddCommGroup H] (φ : G ≃+ H) (α : Ordinal.{u_1}) : ↥(pSocleAt p α) ≃+ ↥(pSocleAt p α)

Restrict a group isomorphism to the p-socles at the same ordinal stage.

Equations

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

noncomputable def UlmsTheorem.ulmQuotientMapIso (p : ℕ) [hp : Fact (Nat.Prime p)] {G H : Type u} [AddCommGroup G] [AddCommGroup H] (φ : G ≃+ H) (α : Ordinal.{u_1}) : ulmQuotient p α ≃+ ulmQuotient p α

An isomorphism induces an isomorphism on the classical Ulm quotients.

Equations

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

theorem UlmsTheorem.ulmInvariant_iso_invariant (p : ℕ) [hp : Fact (Nat.Prime p)] {G H : Type u} [AddCommGroup G] [AddCommGroup H] (φ : G ≃+ H) (α : Ordinal.{u_1}) : ulmInvariant p α = ulmInvariant p α

Isomorphic groups have equal Ulm invariants.