LeanAPAP.Mathlib.Algebra.Group.AddChar

TODO #

Rename

map_add_mul → map_add_eq_mul
map_zero_one → map_zero_eq_one
map_nsmul_pow → map_nsmul_eq_pow

source

instance AddChar.instAddCommMonoid {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] :

AddCommMonoid (AddChar G R)

Equations

AddChar.instAddCommMonoid = Additive.addCommMonoid

source

def AddChar.toMonoidHomEquiv' {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] :

AddChar G R ≃ (Multiplicative G →* R)

Interpret an additive character as a monoid homomorphism.

Equations

AddChar.toMonoidHomEquiv' = AddChar.toMonoidHomEquiv G R

Instances For

source

@[simp]

theorem AddChar.coe_toMonoidHomEquiv' {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : AddChar G R) :

⇑(AddChar.toMonoidHomEquiv' ψ) = ⇑ψ ∘ ⇑Multiplicative.toAdd

source

@[simp]

theorem AddChar.coe_toMonoidHomEquiv'_symm {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : Multiplicative G →* R) :

⇑(AddChar.toMonoidHomEquiv'.symm ψ) = ⇑ψ ∘ ⇑Multiplicative.ofAdd

source

@[simp]

theorem AddChar.toMonoidHomEquiv'_apply {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : AddChar G R) (a : Multiplicative G) :

(AddChar.toMonoidHomEquiv' ψ) a = ψ (Multiplicative.toAdd a)

source

@[simp]

theorem AddChar.toMonoidHomEquiv'_symm_apply {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : Multiplicative G →* R) (a : G) :

(AddChar.toMonoidHomEquiv'.symm ψ) a = ψ (Multiplicative.ofAdd a)

source

@[simp]

theorem AddChar.toMonoidHomEquiv'_zero {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] :

AddChar.toMonoidHomEquiv' 0 = 1

source

@[simp]

theorem AddChar.toMonoidHomEquiv'_symm_one {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] :

AddChar.toMonoidHomEquiv'.symm 1 = 0

source

@[simp]

theorem AddChar.toMonoidHomEquiv'_add {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : AddChar G R) (φ : AddChar G R) :

AddChar.toMonoidHomEquiv' (ψ + φ) = AddChar.toMonoidHomEquiv' ψ * AddChar.toMonoidHomEquiv' φ

source

@[simp]

theorem AddChar.toMonoidHomEquiv'_symm_mul {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : Multiplicative G →* R) (φ : Multiplicative G →* R) :

AddChar.toMonoidHomEquiv'.symm (ψ * φ) = AddChar.toMonoidHomEquiv'.symm ψ + AddChar.toMonoidHomEquiv'.symm φ

source

def AddChar.toAddMonoidHomEquiv' {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] :

AddChar G R ≃ (G →+ Additive R)

Interpret an additive character as a monoid homomorphism.

Equations

AddChar.toAddMonoidHomEquiv' = AddChar.toAddMonoidHomEquiv G R

Instances For

source

@[simp]

theorem AddChar.coe_toAddMonoidHomEquiv' {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : AddChar G R) :

⇑(AddChar.toAddMonoidHomEquiv' ψ) = ⇑Additive.ofMul ∘ ⇑ψ

source

@[simp]

theorem AddChar.coe_toAddMonoidHomEquiv'_symm {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : G →+ Additive R) :

⇑(AddChar.toAddMonoidHomEquiv'.symm ψ) = ⇑Additive.toMul ∘ ⇑ψ

source

@[simp]

theorem AddChar.toAddMonoidHomEquiv'_apply {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : AddChar G R) (a : G) :

(AddChar.toAddMonoidHomEquiv' ψ) a = Additive.ofMul (ψ a)

source

@[simp]

theorem AddChar.toAddMonoidHomEquiv'_symm_apply {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : G →+ Additive R) (a : G) :

(AddChar.toAddMonoidHomEquiv'.symm ψ) a = Additive.toMul (ψ a)

source

theorem AddChar.eq_one_iff {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] {ψ : AddChar G R} :

ψ = 0 ↔ ∀ (x : G), ψ x = 1

source

theorem AddChar.ne_one_iff {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] {ψ : AddChar G R} :

ψ ≠ 0 ↔ ∃ (x : G), ψ x ≠ 1

source

@[simp]

theorem AddChar.coe_one {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] :

⇑1 = 1

source

@[simp]

theorem AddChar.coe_mul {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : AddChar G R) (χ : AddChar G R) :

⇑(ψ * χ) = ⇑ψ * ⇑χ

source

@[simp]

theorem AddChar.coe_pow {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (n : ℕ) (ψ : AddChar G R) :

⇑(ψ ^ n) = ⇑ψ ^ n

source

theorem AddChar.eq_zero_iff {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] {ψ : AddChar G R} :

ψ = 0 ↔ ∀ (x : G), ψ x = 1

source

theorem AddChar.ne_zero_iff {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] {ψ : AddChar G R} :

ψ ≠ 0 ↔ ∃ (x : G), ψ x ≠ 1

source

@[simp]

theorem AddChar.coe_zero {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] :

⇑0 = 1

source

theorem AddChar.zero_apply {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (a : G) :

0 a = 1

source

@[simp]

theorem AddChar.coe_eq_zero {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] {ψ : AddChar G R} :

⇑ψ = 1 ↔ ψ = 0

source

@[simp]

theorem AddChar.coe_add {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : AddChar G R) (χ : AddChar G R) :

⇑(ψ + χ) = ⇑ψ * ⇑χ

source

theorem AddChar.add_apply {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (ψ : AddChar G R) (χ : AddChar G R) (a : G) :

(ψ + χ) a = ψ a * χ a

source

@[simp]

theorem AddChar.coe_nsmul {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (n : ℕ) (ψ : AddChar G R) :

⇑(n • ψ) = ⇑ψ ^ n

source

theorem AddChar.nsmul_apply {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (n : ℕ) (ψ : AddChar G R) (a : G) :

(ψ ^ n) a = ψ a ^ n

source

@[simp]

theorem AddChar.coe_sum {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] {ι : Type u_4} (s : Finset ι) (ψ : ι → AddChar G R) :

⇑(Finset.sum s fun (i : ι) => ψ i) = Finset.prod s fun (i : ι) => ⇑(ψ i)

source

theorem AddChar.sum_apply {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] {ι : Type u_4} (s : Finset ι) (ψ : ι → AddChar G R) (a : G) :

(Finset.sum s fun (i : ι) => ψ i) a = Finset.prod s fun (i : ι) => (ψ i) a

source

noncomputable instance AddChar.instDecidableEqAddCharToMonoid {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] :

DecidableEq (AddChar G R)

Equations

AddChar.instDecidableEqAddCharToMonoid = Classical.decEq (AddChar G R)

source

@[simp]

theorem AddChar.compAddMonoidHom_apply {G : Type u_1} {H : Type u_2} {R : Type u_3} [AddMonoid G] [AddMonoid H] [CommMonoid R] (ψ : AddChar H R) (f : G →+ H) (a : G) :

(AddChar.compAddMonoidHom ψ f) a = ψ (f a)

source

theorem AddChar.compAddMonoidHom_injective_left {G : Type u_1} {H : Type u_2} {R : Type u_3} [AddMonoid G] [AddMonoid H] [CommMonoid R] (f : G →+ H) (hf : Function.Surjective ⇑f) :

Function.Injective fun (ψ : AddChar H R) => AddChar.compAddMonoidHom ψ f

source

theorem AddChar.compAddMonoidHom_injective_right {G : Type u_1} {H : Type u_2} {R : Type u_3} [AddMonoid G] [AddMonoid H] [CommMonoid R] (ψ : AddChar H R) (hψ : Function.Injective ⇑ψ) :

Function.Injective fun (f : G →+ H) => AddChar.compAddMonoidHom ψ f

source

def AddChar.doubleDualEmb {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] :

G →+ AddChar (AddChar G R) R

The double dual embedding.

Equations

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

Instances For

source

@[simp]

theorem AddChar.doubleDualEmb_apply {G : Type u_1} {R : Type u_3} [AddMonoid G] [CommMonoid R] (a : G) (ψ : AddChar G R) :

(AddChar.doubleDualEmb a) ψ = ψ a

source

theorem AddChar.map_sub_eq_div {G : Type u_1} {R : Type u_3} [AddGroup G] [DivisionCommMonoid R] (ψ : AddChar G R) (x : G) (y : G) :

ψ (x - y) = ψ x / ψ y

source

theorem AddChar.injective_iff {G : Type u_1} {R : Type u_3} [AddGroup G] [DivisionCommMonoid R] {ψ : AddChar G R} :

Function.Injective ⇑ψ ↔ ∀ ⦃x : G⦄, ψ x = 1 → x = 0

source

theorem AddChar.sum_eq_ite {G : Type u_1} {R : Type u_3} [AddGroup G] [Fintype G] [CommSemiring R] [IsDomain R] (ψ : AddChar G R) :

(Finset.sum Finset.univ fun (a : G) => ψ a) = if ψ = 0 then ↑(Fintype.card G) else 0

source

theorem AddChar.sum_eq_zero_iff_ne_zero {G : Type u_1} {R : Type u_3} [AddGroup G] [Fintype G] [CommSemiring R] [IsDomain R] [CharZero R] {ψ : AddChar G R} :

(Finset.sum Finset.univ fun (x : G) => ψ x) = 0 ↔ ψ ≠ 0

source

theorem AddChar.sum_ne_zero_iff_eq_zero {G : Type u_1} {R : Type u_3} [AddGroup G] [Fintype G] [CommSemiring R] [IsDomain R] [CharZero R] {ψ : AddChar G R} :

(Finset.sum Finset.univ fun (x : G) => ψ x) ≠ 0 ↔ ψ = 0

source

instance AddChar.instAddCommGroupAddCharToAddMonoidToSubNegMonoidToAddGroupToMonoid {G : Type u_1} {R : Type u_3} [AddCommGroup G] [CommMonoid R] :

AddCommGroup (AddChar G R)

The additive characters on a commutative additive group form a commutative group.

Equations

AddChar.instAddCommGroupAddCharToAddMonoidToSubNegMonoidToAddGroupToMonoid = Additive.addCommGroup

source

@[simp]

theorem AddChar.neg_apply {G : Type u_1} {R : Type u_3} [AddCommGroup G] [CommMonoid R] (ψ : AddChar G R) (a : G) :

(-ψ) a = ψ (-a)

source

@[simp]

theorem AddChar.sub_apply {G : Type u_1} {R : Type u_3} [AddCommGroup G] [CommMonoid R] (ψ : AddChar G R) (χ : AddChar G R) (a : G) :

(ψ - χ) a = ψ a * χ (-a)

source

@[simp]

theorem AddChar.map_zsmul_eq_zpow {G : Type u_1} {R : Type u_3} [AddCommGroup G] [DivisionCommMonoid R] (ψ : AddChar G R) (n : ℤ) (a : G) :

ψ (n • a) = ψ a ^ n

source

theorem AddChar.map_neg_eq_inv {G : Type u_1} {R : Type u_3} [AddCommGroup G] [DivisionCommMonoid R] (ψ : AddChar G R) (x : G) :

ψ (-x) = (ψ x)⁻¹

source

theorem AddChar.neg_apply' {G : Type u_1} {R : Type u_3} [AddCommGroup G] [DivisionCommMonoid R] (ψ : AddChar G R) (x : G) :

(-ψ) x = (ψ x)⁻¹

source

theorem AddChar.sub_apply' {G : Type u_1} {R : Type u_3} [AddCommGroup G] [DivisionCommMonoid R] (ψ : AddChar G R) (χ : AddChar G R) (a : G) :

(ψ - χ) a = ψ a / χ a