OAI/Algebra/AuslanderReiten/Evaluation/ConcreteFreePure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.ExternalBalanced.totalFreeEvaluation_canonical_pure line 23

   Source comment

   State the generic value in the canonical-input presentation used by endpoint insertion.

   private theorem totalFreeEvaluation_canonical_pure (a b : A) (c d : B) (m : M) (n : N) :
       totalFreeEvaluation k A B M N e f
         ((productEvaluation k A B X Y).map
           (ExternalTensor.inclusion k (AbsoluteBar.Enveloping k A) (AbsoluteBar.Enveloping k B) P Q 0 0 0 rfl)
           (BalancedTensor.tmul
             ((bimoduleCoordinates k A B ((P).X 0) ((Q).X 0)).symm
               ((⟨a ⊗ₜ[k] b⟩ : EnvelopingBimodule k A ((P).X 0)) ⊗ₜ[k]
                (⟨c ⊗ₜ[k] d⟩ : EnvelopingBimodule k B ((Q).X 0))))
             (ExternalTensor.canonicalTmul k A B M N m n))) =
         (e (b • m) • a) ⊗ₜ[k] (f (d • n) • c) :=
   …

   Mentions: OAI.ArExplicit.A, OAI.ArExplicit.ExternalBalanced.totalFreeEvaluation, OAI.ArExplicit.ExternalBalanced.productEvaluation, OAI.ArExplicit.ExternalTensor.inclusion, OAI.ArExplicit.AbsoluteBar.Enveloping, OAI.ArExplicit.BalancedTensor.tmul, OAI.ArExplicit.ExternalBalanced.bimoduleCoordinates, OAI.ArExplicit.EnvelopingBimodule, OAI.ArExplicit.ExternalTensor.canonicalTmul

2. theorem OAI.ArExplicit.T.endpointEvaluation_pure line 52
3. theorem OAI.ArExplicit.T.evaluatedPairValue line 68
4. theorem OAI.ArExplicit.T.rawEndpointPairValue line 78
5. theorem OAI.ArExplicit.T.freeCoordinateRaw_endpoint_pure line 84