The nonisomorphism proofs component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperNonisomorphism.PaperEll : Type

The PaperEll construction used in the Connes rigidity formalization.

Equations

• Connes.PaperNonisomorphism.PaperEll = (Connes.Construction.PaperKernel.VStar × Connes.Construction.k)

def Connes.PaperNonisomorphism.paperEllMap (q : ↥Construction.PaperKernel.Q) : PaperEll →ₗ[Construction.k] PaperEll

The paperEllMap construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

def Connes.PaperNonisomorphism.paperEllRepresentation : Representation Construction.k (↥Construction.PaperKernel.Q) PaperEll

The paperEllRepresentation construction used in the Connes rigidity formalization.

Equations

• Connes.PaperNonisomorphism.paperEllRepresentation = { toFun := Connes.PaperNonisomorphism.paperEllMap, map_one' := Connes.PaperNonisomorphism.paperEllRepresentation._proof_2, map_mul' := ⋯ }

def Connes.PaperNonisomorphism.paperEllVStarRepresentation : Representation Construction.k (↥Construction.PaperKernel.Q) Construction.PaperKernel.VStar

The paperEllVStarRepresentation construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

def Connes.PaperNonisomorphism.paperEllScalarRepresentation : Representation Construction.k (↥Construction.PaperKernel.Q) Construction.k

The paperEllScalarRepresentation construction used in the Connes rigidity formalization.

Equations

• Connes.PaperNonisomorphism.paperEllScalarRepresentation = Representation.trivial Connes.Construction.k (↥Connes.Construction.PaperKernel.Q) Connes.Construction.k

def Connes.PaperNonisomorphism.paperEllInclusionLinear : Construction.PaperKernel.VStar →ₗ[Construction.k] PaperEll

The paperEllInclusionLinear construction used in the Connes rigidity formalization.

Equations

• Connes.PaperNonisomorphism.paperEllInclusionLinear = { toFun := fun (f : Connes.Construction.PaperKernel.VStar) => (f, 0), map_add' := ⋯, map_smul' := ⋯ }

def Connes.PaperNonisomorphism.paperEllInclusionIntertwining : paperEllVStarRepresentation.IntertwiningMap paperEllRepresentation

The paperEllInclusionIntertwining construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

def Connes.PaperNonisomorphism.paperEllProjectionLinear : PaperEll →ₗ[Construction.k] Construction.k

The paperEllProjectionLinear construction used in the Connes rigidity formalization.

Equations

• Connes.PaperNonisomorphism.paperEllProjectionLinear = { toFun := fun (p : Connes.PaperNonisomorphism.PaperEll) => p.2, map_add' := ⋯, map_smul' := ⋯ }

def Connes.PaperNonisomorphism.paperEllProjectionIntertwining : paperEllRepresentation.IntertwiningMap paperEllScalarRepresentation

The paperEllProjectionIntertwining construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

def Connes.PaperNonisomorphism.paperEllInclusion : paperEllVStarRepresentation.asModule →ₗ[Ring] paperEllRepresentation.asModule

The paperEllInclusion construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

def Connes.PaperNonisomorphism.paperEllProjection : paperEllRepresentation.asModule →ₗ[Ring] paperEllScalarRepresentation.asModule

The paperEllProjection construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem Connes.PaperNonisomorphism.paperEll_projection_surjective : Function.Surjective ⇑paperEllProjection

theorem Connes.PaperNonisomorphism.paperEll_exact : Function.Exact ⇑paperEllInclusion ⇑paperEllProjection

theorem Connes.PaperNonisomorphism.paperEll_extension_not_splits : ¬∃ (section_ : paperEllScalarRepresentation.asModule →ₗ[Ring] paperEllRepresentation.asModule), paperEllProjection ∘ₗ section_ = LinearMap.id

theorem Connes.PaperNonisomorphism.paperEll_not_semisimple : ¬IsSemisimpleModule Ring paperEllRepresentation.asModule