Duality for finite abelian groups

Let G be a finite abelian group.

For M a commutative monoid that has enough nth roots of unity, where n is the exponent of G, the main results in this file are:

• CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity: Homomorphisms G →* Mˣ separate elements of G.
• CommGroup.monoidHom_mulEquiv_self_of_hasEnoughRootsOfUnity: G is isomorphic to G →* Mˣ.
• CommGroup.monoidHomMonoidHomEquiv: G is isomorphic to its double dual (G →* Mˣ) →* Mˣ.
• CommGroup.subgroupOrderIsoSubgroupMonoidHom: the order reversing bijection that sends a subgroup of G to its dual subgroup in G →* Mˣ.

theorem CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] {a : G} (ha : a ≠ 1) : ∃ (φ : G →* Mˣ), φ a ≠ 1

If G is a finite commutative group of exponent n and M is a commutative monoid with enough nth roots of unity, then for each a ≠ 1 in G, there exists a group homomorphism φ : G → Mˣ such that φ a ≠ 1.

@[simp]

theorem CommGroup.forall_apply_eq_apply_iff (G : Type u_1) {M : Type u_2} [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] {g g' : G} : (∀ (φ : G →* Mˣ), φ g = φ g') ↔ g = g'

theorem CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] : Nonempty ((G →* Mˣ) ≃* G)

A finite commutative group G is (noncanonically) isomorphic to the group G →* Mˣ when M is a commutative monoid with enough nth roots of unity, where n is the exponent of G.

theorem CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] : Nat.card (G →* Mˣ) = Nat.card G

theorem MonoidHom.restrict_surjective {G : Type u_1} (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G) : Function.Surjective ⇑(restrictHom H Mˣ)

Let G be a finite commutative group and let H be a subgroup. If M is a commutative monoid such that G →* Mˣ and H →* Mˣ are both finite (this is the case for example if M is a commutative domain) and with enough nth roots of unity, where n is the exponent of G, then any homomorphism H →* Mˣ can be extended to an homomorphism G →* Mˣ.

@[simp]

theorem CommGroup.forall_monoidHom_apply_eq_one_iff {G : Type u_1} (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G) (x : G) : (∀ (φ : G →* Mˣ), (∀ y ∈ H, φ y = 1) → φ x = 1) ↔ x ∈ H

noncomputable def CommGroup.monoidHomMonoidHomEquiv (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] : ((G →* Mˣ) →* Mˣ) ≃* G

The MulEquiv between the double dual (G →* Mˣ) →* Mˣ of a finite commutative group G and itself where M is a commutative monoid with enough nth roots of unity, where n is the exponent of G. The image g of η : (G →* Mˣ) →* Mˣ is such that, for all φ : G →* Mˣ, we have φ g = η g, see CommGroup.apply_monoidHomMonoidHomEquiv.

Equations

• CommGroup.monoidHomMonoidHomEquiv G M = (MulEquiv.mk' (Equiv.ofBijective (fun (g : G) => { toFun := fun (φ : G →* Mˣ) => φ g, map_one' := ⋯, map_mul' := ⋯ }) ⋯) ⋯).symm

@[simp]

theorem CommGroup.monoidHomMonoidHomEquiv_symm_apply_apply (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (a✝ : G) (φ : G →* Mˣ) : ((monoidHomMonoidHomEquiv G M).symm a✝) φ = φ a✝

@[simp]

theorem CommGroup.apply_monoidHomMonoidHomEquiv {G : Type u_1} (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (φ : G →* Mˣ) (η : (G →* Mˣ) →* Mˣ) : φ ((monoidHomMonoidHomEquiv G M) η) = η φ

noncomputable def CommGroup.subgroupOrderIsoSubgroupMonoidHom (G : Type u_1) (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] : Subgroup G ≃o (Subgroup (G →* Mˣ))ᵒᵈ

The order reversing bijection that sends a subgroup of G to its dual subgroup in G →* Mˣ where G is a finite commutative group and M is a commutative monoid with enough nth roots of unity, where n is the exponent of G.

Equations

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

@[simp]

theorem CommGroup.mem_subgroupOrderIsoSubgroupMonoidHom_iff {G : Type u_1} (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G) (φ : G →* Mˣ) : φ ∈ OrderDual.ofDual ((subgroupOrderIsoSubgroupMonoidHom G M) H) ↔ ∀ g ∈ H, φ g = 1

@[simp]

theorem CommGroup.mem_subgroupOrderIsoSubgroupMonoidHom_symm_iff {G : Type u_1} (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (Φ : Subgroup (G →* Mˣ)) (g : G) : g ∈ (subgroupOrderIsoSubgroupMonoidHom G M).symm (OrderDual.toDual Φ) ↔ ∀ φ ∈ Φ, φ g = 1