liftEquiv — Mathlib

English

If two lifts correspond to equal f and g with equal commuting data, they are equal as algebra homomorphisms.

Русский

Если два лифта соответствуют равным f и g и одинаковым данным сопряжённости, они равны как алгебраические гомоморфизмы.

LaTeX

$$$\\mathrm{lift}\; f\\; g\\; hfg = \\mathrm{lift}\\; f'\\; g'\\; hfg'\\quad\\text{when } f=f', g=g', hfg=hfg'.$$$

Lean4

/-- The universal property of the tensor product of algebras.

Pairs of algebra morphisms that commute are equivalent to algebra morphisms from the tensor product.

This is `Algebra.TensorProduct.lift` as an equivalence.

See also `GradedTensorProduct.liftEquiv` for an alternative commutativity requirement for graded
algebra. -/
@[simps]
def liftEquiv : { fg : (A →ₐ[S] C) × (B →ₐ[R] C) // ∀ x y, Commute (fg.1 x) (fg.2 y) } ≃ ((A ⊗[R] B) →ₐ[S] C)
    where
  toFun fg := lift fg.val.1 fg.val.2 fg.prop
  invFun
    f' :=
    ⟨(f'.comp includeLeft, (f'.restrictScalars R).comp includeRight), fun _ _ =>
      ((Commute.one_right _).tmul (Commute.one_left _)).map f'⟩
  left_inv fg := by ext <;> simp
  right_inv f' := by ext <;> simp

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