lift

Mathlib.GroupTheory.Congruence.Hom

URI: https://scilib.ai/kg/mathlib#Con.lift

Lean4

/-- The homomorphism on the quotient of a monoid by a congruence relation `c` induced by a
homomorphism constant on `c`'s equivalence classes. -/
@[to_additive /-- The homomorphism on the quotient of an `AddMonoid` by an additive congruence
    relation `c` induced by a homomorphism constant on `c`'s equivalence classes. -/
    ]
def lift (H : c ≤ ker f) : c.Quotient →* P
    where
  toFun x := (Con.liftOn x f) fun _ _ h => H h
  map_one' := by rw [← f.map_one]; rfl
  map_mul' x
    y :=
    Con.induction_on₂ x y fun m n => by
      dsimp only [← coe_mul, Con.liftOn_coe]
      rw [map_mul]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru