lift — Mathlib

English

Given a function f: X → A into an A that is an R-algebra, lift R f yields a unique R-algebra homomorphism FreeAlgebra R X → A extending f.

Русский

Для функции f: X → A в A, являющуюся R-алгеброй, существует единственный гомоморфизм R-алгебр Lift, который распространяет f на FreeAlgebra R X.

LaTeX

$$$\mathrm{lift}: (X \to A) \simeq (\mathrm{FreeAlgebra}(R,X) \to_A A)$$$

Lean4

/-- Given a function `f : X → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
of `f` to a morphism of `R`-algebras `FreeAlgebra R X → A`. -/
@[irreducible]
def lift : (X → A) ≃ (FreeAlgebra R X →ₐ[R] A) :=
  { toFun := liftAux R
    invFun := fun F ↦ F ∘ ι R
    left_inv := fun f ↦ by
      ext
      simp only [Function.comp_apply, ι_def]
      rfl
    right_inv := fun F ↦ by
      ext t
      rcases t with ⟨x⟩
      induction x with
      | of =>
        change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
        simp only [Function.comp_apply, ι_def]
      | ofScalar x =>
        change algebraMap _ _ x = F (algebraMap _ _ x)
        rw [AlgHom.commutes F _]
      | add a b ha hb =>
        -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses
                -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X

        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
        rw [map_add, map_add, ha, hb]
      | mul a b ha hb =>
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
        rw [map_mul, map_mul, ha, hb] }

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