FactorTensorInjection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Algebraic injectivity for commuting faithful factor restrictions. This is the factor-representation step in Tomiyama's Theorem 5, specialized to the product representation needed for tensor-ideal separation.

theorem OAI.WeakPureInfiniteness.factor_tensor_lift_injective line 19