lift — Mathlib

English

There is a universal lifting of a function f from representatives to FiniteMulArchimedeanClass M.

Русский

Существует обобщённое поднятие функции f с представителей до FiniteMulArchimedeanClass M.

LaTeX

$$$\text{lift } f h : FiniteMulArchimedeanClass M \to α$$$

Lean4

/-- Lift a `f : {a : M // a ≠ 1} → α` function to `FiniteMulArchimedeanClass M → α`. -/
@[to_additive /-- Lift a `f : {a : M // a ≠ 0} → α` function to `FiniteArchimedeanClass M → α`. -/
    ]
def lift {α : Type*} (f : { a : M // a ≠ 1 } → α)
    (h : ∀ (a b : { a : M // a ≠ 1 }), mk a.val a.prop = mk b.val b.prop → f a = f b) :
    FiniteMulArchimedeanClass M → α := fun ⟨A, hA⟩ ↦
  by
  refine
    (MulArchimedeanClass.lift (fun b ↦ if h : b = 1 then ⊤ else WithTop.some (f ⟨b, h⟩)) (fun a b h' ↦ ?_) A).untop ?_
  · simp only
    split_ifs with ha hb hb
    · rfl
    · exact (hb (MulArchimedeanClass.mk_eq_top_iff.mp (ha ▸ h').symm)).elim
    · exact (ha (MulArchimedeanClass.mk_eq_top_iff.mp (by apply hb ▸ h'))).elim
    · rw [h ⟨a, ha⟩ ⟨b, hb⟩ (by simpa [mk] using h')]
  · induction A using MulArchimedeanClass.ind with
    | mk a
    simpa using MulArchimedeanClass.mk_eq_top_iff.not.mp hA

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