OAI/Algebra/AuslanderReiten/Ext/ExternalRegularEvaluation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.BarBalanced.nativeEndpointIso_tmul line 18
2. theorem OAI.ArExplicit.BarBalanced.regularMap_tmul_of_smul line 26
3. theorem OAI.ArExplicit.BarBalanced.namedRegularMap_tmul_of_smul line 33
4. theorem OAI.ArExplicit.ExternalBalanced.exterior_raw_hom_ext line 61

   Source comment

   Keep the scalar-ring and evaluation-object presentations used by the endpoint maps. This avoids expanding their tensor-module structures when specializing extensionality to the degree-zero bar objects.

   private theorem exterior_raw_hom_ext
       (M : ModuleCat.{u} (AbsoluteBar.Enveloping k A)) (N : ModuleCat.{u} (AbsoluteBar.Enveloping k B))
       (Z : ModuleCat.{u} (A ⊗[k] B))
       (f : (productEvaluation k A B X Y).obj
         (ExternalTensor.moduleObject k (A ⊗[k] Aᵐᵒᵖ) (B ⊗[k] Bᵐᵒᵖ) M N) ⟶ Z)
       (g : (E).obj (ExternalTensor.envelopingObject k A B
         (ExternalTensor.moduleObject k (A ⊗[k] Aᵐᵒᵖ) (B ⊗[k] Bᵐᵒᵖ) M N)) ⟶ Z)
       (h : ∀ (a : EnvelopingBimodule k A M) (b : EnvelopingBimodule k B N) (x : X) (y : Y),
         f (BalancedTensor.tmul ((bimoduleCoordinates k A B M N).symm (a ⊗ₜ[k] b))
           ((ExternalTensor.moduleScalarCoordinates k A B X Y).symm (x ⊗ₜ[k] y))) =
         g (BalancedTensor.tmul ((bimoduleCoordinates k A B M N).symm (a ⊗ₜ[k] b))
           ((ExternalTensor.moduleScalarCoordinates k A B X Y).symm (x ⊗ₜ[k] y)))) : f = g :=
   …

   Mentions: OAI.ArExplicit.AbsoluteBar.Enveloping, OAI.ArExplicit.A, OAI.ArExplicit.ExternalBalanced.productEvaluation, OAI.ArExplicit.ExternalTensor.moduleObject, OAI.ArExplicit.ExternalTensor.envelopingObject, OAI.ArExplicit.EnvelopingBimodule, OAI.ArExplicit.BalancedTensor.tmul, OAI.ArExplicit.ExternalBalanced.bimoduleCoordinates, OAI.ArExplicit.ExternalTensor.moduleScalarCoordinates

5. def OAI.ArExplicit.ExternalBalanced.factorRegularEndpoint line 75
6. def OAI.ArExplicit.ExternalBalanced.productRegularEndpoint line 81
7. theorem OAI.ArExplicit.ExternalBalanced.factorRegularEndpoint_pure line 89
8. theorem OAI.ArExplicit.ExternalBalanced.productRegularEndpoint_eq_map line 103
9. theorem OAI.ArExplicit.ExternalBalanced.productRegularEndpoint_scalar_pure line 110
10. theorem OAI.ArExplicit.ExternalBalanced.productRegularEndpoint_scalar_action line 118
11. abbrev OAI.ArExplicit.ExternalBalanced.productRegularEndpointPureProof line 129
12. theorem OAI.ArExplicit.ExternalBalanced.productRegularEndpoint_pure line 141
13. theorem OAI.ArExplicit.ExternalBalanced.regularEndpoint_pure_eq line 147
14. theorem OAI.ArExplicit.ExternalBalanced.regularEndpoint_ext line 155
15. theorem OAI.ArExplicit.ExternalBalanced.regularEndpoint_eq_aux line 159
16. theorem OAI.ArExplicit.ExternalBalanced.regularEndpoint_eq line 167