Theorems · Definition · commutative algebra
CharacterModule
(A : Type uA) → [AddCommGroup A] → Type uA
The character module of an abelian group A in the unit rational circle is A⋆ := Hom_ℤ(A, ℚ ⧸ ℤ).
- Defined in
- Mathlib.Algebra.Module.CharacterModule
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- AddMonoidHomproof · cited by 3,230
- AddCircleproof · cited by 189
Cited by33
Results whose statement or proof uses this declaration.
- CharacterModule.dualstatement and proof · cited by 13
- Module.Flat.iff_rTensor_injective'proof · cited by 4
- CharacterModule.extstatement and proof · cited by 4
- CharacterModule.homEquivstatement · cited by 4
- CharacterModule.dual_surjective_of_injectivestatement · cited by 2
- CharacterModule.eq_zero_of_character_applystatement and proof · cited by 2
- CharacterModule.intproof · cited by 2
- CharacterModule.ofSpanSingletonstatement · cited by 2
- Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMapstatement and proof · cited by 1
- AddCommGrpCat.isColimit_iff_bijective_descproof · cited by 1
- CharacterModule.congrstatement · cited by 1
- CharacterModule.currystatement and proof · cited by 1