Documentation

TauCeti.RingTheory.RootsOfUnity.Map

Maps on groups of p-power roots of unity #

A monoid homomorphism restricts to a homomorphism on the groups of p-power roots of unity. These maps preserve identity and composition; a monoid isomorphism yields a group isomorphism.

source
def TauCeti.pPowerRootsOfUnityMap (p : ℕ) {K : Type u_1} {L : Type u_2} [CommMonoid K] [CommMonoid L] (f : K →* L) :
↥(pPowerRootsOfUnity p K) →* ↥(pPowerRootsOfUnity p L)

The map on p-power roots of unity induced by a monoid homomorphism.

Instances For
    source
    @[simp]
    theorem TauCeti.pPowerRootsOfUnityMap_apply (p : ℕ) {K : Type u_1} {L : Type u_2} [CommMonoid K] [CommMonoid L] (f : K →* L) (x : ↥(pPowerRootsOfUnity p K)) :
    ↑((pPowerRootsOfUnityMap p f) x) = (Units.map f) ↑x

    The induced map is the usual map on units.

    source
    theorem TauCeti.pPowerRootsOfUnityMap_injective (p : ℕ) {K : Type u_1} {L : Type u_2} [CommMonoid K] [CommMonoid L] (f : K →* L) (hf : Function.Injective ⇑f) :
    Function.Injective ⇑(pPowerRootsOfUnityMap p f)

    Injective monoid homomorphisms induce injective maps on p-power roots of unity.

    source
    @[simp]
    theorem TauCeti.pPowerRootsOfUnityMap_id (p : ℕ) {K : Type u_1} [CommMonoid K] :
    pPowerRootsOfUnityMap p (MonoidHom.id K) = MonoidHom.id ↥(pPowerRootsOfUnity p K)

    The identity monoid map acts trivially on the p-power roots.

    source
    @[simp]
    theorem TauCeti.pPowerRootsOfUnityMap_comp (p : ℕ) {K : Type u_1} {L : Type u_2} [CommMonoid K] [CommMonoid L] {M : Type u_3} [CommMonoid M] (f : K →* L) (g : L →* M) :
    pPowerRootsOfUnityMap p (g.comp f) = (pPowerRootsOfUnityMap p g).comp (pPowerRootsOfUnityMap p f)

    Root-group maps compose as the underlying monoid maps do.

    source
    noncomputable def TauCeti.pPowerRootsOfUnityEquiv (p : ℕ) {K : Type u_1} {L : Type u_2} [CommMonoid K] [CommMonoid L] (f : K ≃* L) :
    ↥(pPowerRootsOfUnity p K) ≃* ↥(pPowerRootsOfUnity p L)

    A monoid isomorphism identifies its two groups of p-power roots of unity.

    Instances For
      source
      @[simp]
      theorem TauCeti.pPowerRootsOfUnityEquiv_apply (p : ℕ) {K : Type u_1} {L : Type u_2} [CommMonoid K] [CommMonoid L] (f : K ≃* L) (x : ↥(pPowerRootsOfUnity p K)) :
      ↑((pPowerRootsOfUnityEquiv p f) x) = (Units.map f.toMonoidHom) ↑x

      The group isomorphism acts by the given monoid isomorphism on units.

      source
      @[simp]
      theorem TauCeti.pPowerRootsOfUnityEquiv_symm (p : ℕ) {K : Type u_1} {L : Type u_2} [CommMonoid K] [CommMonoid L] (f : K ≃* L) :
      (pPowerRootsOfUnityEquiv p f).symm = pPowerRootsOfUnityEquiv p f.symm

      The inverse root-group equivalence is induced by the inverse monoid equivalence.