TracialGeneratedAlgebra.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing to the algebra normally generated by two free factors gives the intrinsic reduced-product generation hypothesis. Only ordinary L² density of the generating algebra is used; no word decomposition or operator estimate is assumed here.

theorem OAI.KadisonSimilarity.factorAlgebra_map_subtype line 18
theorem OAI.KadisonSimilarity.TracialCornerGeometry.factorsTraciallyGenerate_of_L2_generation line 39
Source documentation
Ordinary ambient L² generation yields the exact intrinsic generation hypothesis for the closed generated algebra's tracial geometry.
```
theorem factorsTraciallyGenerate_of_L2_generation
    (hA : A ≤ L) (hD : D ≤ L)
    (hdense : ∀ a : L, G.vector (a : P) ∈
      closure (Set.range (G.vector.comp (factorAlgebra A D).subtype.toLinearMap))) :
    (G.baseGeometry L).FactorsTraciallyGenerate (A.comap L.subtype) (D.comap L.subtype) := by
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra, OAI.KadisonSimilarity.TracialCornerGeometry.FactorsTraciallyGenerate