Theorems · Definition · group theory
Matrix.ProjGenLinGroup.lift
{n : Type u_1} →
{R : Type u_2} →
[inst : Fintype n] →
[inst_1 : DecidableEq n] →
[inst_2 : CommRing R] →
{M : Type u_3} →
[inst_3 : Monoid M] →
(f : GL n R →* M) → f.comp (Matrix.GeneralLinearGroup.scalar n) = 1 → Matrix.ProjGenLinGroup n R →* MLift a monoid homomorphism f : GL n R →* M that vanishes on all scalar matrices
to a homomorphism from PGL(n, R).
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Fintypestatement and proof · cited by 7,736
- Matrixstatement · cited by 4,303
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- Unitsstatement · cited by 2,804
- Matrix.GeneralLinearGroupstatement and proof · cited by 556
- MonoidHom.compstatement and proof · cited by 469
- Subgroup.centerproof · cited by 121
- Matrix.ProjGenLinGroupstatement · cited by 23
- Matrix.GeneralLinearGroup.scalarstatement and proof · cited by 18
- QuotientGroup.liftproof · cited by 8
Cited by4
Results whose statement or proof uses this declaration.
- Matrix.ProjGenLinGroup.signDetproof · cited by 2
- Matrix.ProjGenLinGroup.mulActionOfGLproof · cited by 1
- Matrix.ProjGenLinGroup.lift_comp_mkstatement and proof · cited by 0
- Matrix.ProjGenLinGroup.lift_mkstatement and proof · cited by 0