Duality for multiplicative characters

Let M be a finite commutative monoid and R a ring that has enough nth roots of unity, where n is the exponent of M. Then the main results of this file are as follows.

Main results

• MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity: multiplicative characters M → R separate elements of Mˣ.

• MulChar.mulEquiv_units: the group of multiplicative characters M → R is (noncanonically) isomorphic to Mˣ.

• MulChar.mulCharEquiv: the MulEquiv between the double dual MulChar (MulChar M R) R of M and Mˣ.

• MulChar.subgroupOrderIsoSubgroupMulChar: The order reversing bijection that sends a subgroup of Mˣ to its dual subgroup in MulChar M R.

instance MulChar.finite {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] [Finite Mˣ] [IsDomain R] : Finite (MulChar M R)

theorem MulChar.exists_apply_ne_one_iff_exists_monoidHom {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] (a : Mˣ) : (∃ (χ : MulChar M R), χ ↑a ≠ 1) ↔ ∃ (φ : Mˣ →* Rˣ), φ a ≠ 1

theorem MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] [Nontrivial R] {a : M} (ha : a ≠ 1) : ∃ (χ : MulChar M R), χ a ≠ 1

If M is a finite commutative monoid and R is a ring that has enough roots of unity, then for each a ≠ 1 in M, there exists a multiplicative character χ : M → R such that χ a ≠ 1.

theorem MulChar.mulEquiv_units (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : Nonempty (MulChar M R ≃* Mˣ)

The group of R-valued multiplicative characters on a finite commutative monoid M is (noncanonically) isomorphic to its unit group Mˣ when R is a ring that has enough roots of unity.

theorem MulChar.card_eq_card_units_of_hasEnoughRootsOfUnity (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : Nat.card (MulChar M R) = Nat.card Mˣ

The cardinality of the group of R-valued multiplicative characters on a finite commutative monoid M is the same as that of its unit group Mˣ when R is a ring that has enough roots of unity.

theorem MulChar.restrictHom_surjective (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] (N : Submonoid M) : Function.Surjective ⇑(restrictHom N R)

Let N be a submonoid of M group and let Rbe a ring with enough roots of unity. Then anyR-value multiplicative character of Ncan be extended to a multiplicative character ofM`.

noncomputable def MulChar.mulCharEquiv (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : MulChar (MulChar M R) R ≃* Mˣ

The MulEquiv between the double dual MulChar (MulChar M R) R of M and Mˣ. The image m of η : MulChar (MulChar M R) R is such that, for all R-valued multiplicative character χ of M, we have χ m = η χ, see MulChar.apply_mulCharEquiv.

Equations

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

@[simp]

theorem MulChar.mulCharEquiv_symm_apply_apply {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] (m : Mˣ) (χ : MulChar M R) : ((mulCharEquiv M R).symm m) χ = χ ↑m

@[simp]

theorem MulChar.apply_mulCharEquiv {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] (χ : MulChar M R) (η : MulChar (MulChar M R) R) : χ ↑((mulCharEquiv M R) η) = η χ

noncomputable def MulChar.subgroupOrderIsoSubgroupMulChar (M : Type u_1) (R : Type u_2) [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] : Subgroup Mˣ ≃o (Subgroup (MulChar M R))ᵒᵈ

The order reversing bijection that sends a subgroup of Mˣ to its dual subgroup in MulChar M R where M is a finite commutative monoid and R is a ring with enough roots of unity.

Equations

• MulChar.subgroupOrderIsoSubgroupMulChar M R = (CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R).trans MulChar.mulEquivToUnitHom.symm.mapSubgroup.dual

@[simp]

theorem MulChar.mem_subgroupOrderIsoSubgroupMulChar_iff {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] {H : Subgroup Mˣ} {χ : MulChar M R} : χ ∈ OrderDual.ofDual ((subgroupOrderIsoSubgroupMulChar M R) H) ↔ ∀ m ∈ H, χ ↑m = 1

@[simp]

theorem MulChar.mem_subgroupOrderIsoSubgroupMulChar_symm_iff {M : Type u_1} {R : Type u_2} [CommMonoid M] [CommRing R] [Finite M] [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] {X : Subgroup (MulChar M R)} {m : Mˣ} : m ∈ (subgroupOrderIsoSubgroupMulChar M R).symm (OrderDual.toDual X) ↔ ∀ χ ∈ X, χ ↑m = 1