OAI/RepresentationTheory/KazhdanLusztig/Frobenius.lean

GitHub source file

198 declarations, 0 contain sorry, 0 declared as axioms

Coxeter Frobenius extensions, tensor duality and translation across reflection pairs.

  1. abbrev OAI.KLInvariance.TitsSpace.SymmetricCoefficient line 18
  2. def OAI.KLInvariance.TitsSpace.coefficientAction line 20
  3. theorem OAI.KLInvariance.TitsSpace.coefficientAction_ι line 23
  4. theorem OAI.KLInvariance.TitsSpace.coefficientAction_simple line 28
  5. theorem OAI.KLInvariance.TitsSpace.coefficientAction_mul line 33
  6. def OAI.KLInvariance.TitsSpace.simpleFixed line 45
  7. abbrev OAI.KLInvariance.TitsSpace.simpleRootPolynomial line 48
  8. theorem OAI.KLInvariance.TitsSpace.simple_involutive line 51
  9. theorem OAI.KLInvariance.TitsSpace.simpleRootPolynomial_ne_zero line 55
  10. theorem OAI.KLInvariance.TitsSpace.simple_anti line 58
  11. theorem OAI.KLInvariance.TitsSpace.simple_divisible line 63
  12. def OAI.KLInvariance.TitsSpace.simpleCoordinates line 68
  13. instance OAI.KLInvariance.TitsSpace.simpleFixed_free line 73
  14. instance OAI.KLInvariance.TitsSpace.simpleFixed_finite line 76
  15. def OAI.KLInvariance.TitsSpace.simpleTrace line 79
  16. def OAI.KLInvariance.TitsSpace.simpleDuality line 83
  17. theorem OAI.KLInvariance.TitsSpace.simpleDuality_apply line 88
  18. def OAI.KLInvariance.FrobeniusDuality.restrictDual line 112
  19. def OAI.KLInvariance.FrobeniusDuality.fiber line 117
  20. theorem OAI.KLInvariance.FrobeniusDuality.fiber_apply line 120
  21. theorem OAI.KLInvariance.FrobeniusDuality.trace_recover_fiber line 124
  22. theorem OAI.KLInvariance.FrobeniusDuality.recover_fiber_smul line 129
  23. def OAI.KLInvariance.FrobeniusDuality.recoverDual line 139
  24. theorem OAI.KLInvariance.FrobeniusDuality.recoverDual_apply line 149
  25. theorem OAI.KLInvariance.FrobeniusDuality.restrict_recover line 152
  26. theorem OAI.KLInvariance.FrobeniusDuality.recover_restrict line 158
  27. def OAI.KLInvariance.FrobeniusDuality.restrictionEquiv line 168
  28. theorem OAI.KLInvariance.FrobeniusDuality.restrictionEquiv_apply line 175
  29. def OAI.KLInvariance.FrobeniusDuality.restrictPairing line 180

    Source documentation

    Restricting an integral perfect pairing along a Frobenius trace is again integral and perfect; no localization or fraction-field argument is used.

     def restrictPairing (p : M ≃ₗ[A] Dual A M) : M ≃ₗ[R] Dual R M :=
…
  30. theorem OAI.KLInvariance.FrobeniusDuality.restrictPairing_apply line 183
  31. def OAI.KLInvariance.FrobeniusDuality.extendPairing line 196
  32. theorem OAI.KLInvariance.FrobeniusDuality.extendPairing_tmul line 201
  33. structure OAI.KLInvariance.FrobeniusDuality.PairedModule line 226
  34. instance OAI.KLInvariance.FrobeniusDuality.(instance at line 235) line 235
  35. def OAI.KLInvariance.FrobeniusDuality.unitPairing line 237
  36. def OAI.KLInvariance.FrobeniusDuality.unitModule line 249
  37. def OAI.KLInvariance.FrobeniusDuality.restrictionBasis line 263
  38. def OAI.KLInvariance.FrobeniusDuality.inducedModule line 270
  39. theorem OAI.KLInvariance.FrobeniusDuality.inducedModule_pairing_tmul line 276
  40. structure OAI.KLInvariance.FrobeniusDuality.PairedBimodule line 295
  41. def OAI.KLInvariance.FrobeniusDuality.unitBimodule line 301
  42. def OAI.KLInvariance.FrobeniusDuality.restrictedRight line 319
  43. def OAI.KLInvariance.FrobeniusDuality.inducedRight line 330
  44. theorem OAI.KLInvariance.FrobeniusDuality.inducedRight_tmul line 333
  45. theorem OAI.KLInvariance.FrobeniusDuality.inducedPairing_balanced line 336
  46. theorem OAI.KLInvariance.FrobeniusDuality.inducedPairing_symmetric line 355
  47. def OAI.KLInvariance.FrobeniusDuality.inducedBimodule line 369
  48. def OAI.KLInvariance.TitsSpace.bottSamelson line 394
  49. abbrev OAI.KLInvariance.TitsSpace.BottSamelsonModule line 399
  50. def OAI.KLInvariance.TitsSpace.bottSamelsonDuality line 401
  51. def OAI.KLInvariance.TitsSpace.bottSamelsonRight line 405
  52. theorem OAI.KLInvariance.TitsSpace.bottSamelson_balanced line 409
  53. theorem OAI.KLInvariance.TitsSpace.bottSamelson_symmetric line 415
  54. theorem OAI.KLInvariance.Graded.homogeneous_of_mul line 435
  55. theorem OAI.KLInvariance.ReflectionFrobenius.trace_difference line 456
  56. theorem OAI.KLInvariance.ReflectionFrobenius.trace_homogeneous line 464
  57. theorem OAI.KLInvariance.ReflectionFrobenius.coordinates_homogeneous line 483
  58. def OAI.KLInvariance.ReflectionFrobenius.reflectionBasis line 522
  59. theorem OAI.KLInvariance.ReflectionFrobenius.reflectionBasis_zero line 525
  60. theorem OAI.KLInvariance.ReflectionFrobenius.reflectionBasis_one line 529
  61. theorem OAI.KLInvariance.ReflectionFrobenius.reflectionBasis_homogeneous line 533
  62. def OAI.KLInvariance.FrobeniusDuality.inducedBasis line 569
  63. theorem OAI.KLInvariance.FrobeniusDuality.inducedBasis_apply line 574
  64. theorem OAI.KLInvariance.FrobeniusDuality.inducedPairing_basis line 580
  65. theorem OAI.KLInvariance.FrobeniusDuality.inducedPairing_basis_homogeneous line 602
  66. theorem OAI.KLInvariance.Graded.algHom_polynomialGrading line 636
  67. def OAI.KLInvariance.ReflectionFrobenius.polynomialLinear line 665
  68. theorem OAI.KLInvariance.ReflectionFrobenius.polynomialLinear_homogeneous line 669
  69. def OAI.KLInvariance.ReflectionFrobenius.polynomialAction line 680
  70. theorem OAI.KLInvariance.ReflectionFrobenius.polynomialAction_linear line 685
  71. theorem OAI.KLInvariance.ReflectionFrobenius.polynomialAction_homogeneous line 690
  72. abbrev OAI.KLInvariance.ReflectionFrobenius.polynomialReflection line 703
  73. theorem OAI.KLInvariance.ReflectionFrobenius.polynomialReflection_involutive line 707
  74. theorem OAI.KLInvariance.ReflectionFrobenius.polynomialReflection_anti line 719
  75. theorem OAI.KLInvariance.ReflectionFrobenius.polynomialLinear_ne_zero line 730
  76. theorem OAI.KLInvariance.ReflectionFrobenius.polynomialReflection_divisible line 736
  77. def OAI.KLInvariance.ReflectionFrobenius.polynomialTrace line 744
  78. theorem OAI.KLInvariance.ReflectionFrobenius.polynomialTrace_homogeneous line 751
  79. def OAI.KLInvariance.TitsSpace.symmetricGrading line 777
  80. theorem OAI.KLInvariance.TitsSpace.mem_symmetricGrading line 782
  81. instance OAI.KLInvariance.TitsSpace.symmetricGrading_decomposition line 792
  82. instance OAI.KLInvariance.TitsSpace.symmetricGrading_graded line 803
  83. theorem OAI.KLInvariance.TitsSpace.symmetricGrading_negative line 815
  84. theorem OAI.KLInvariance.TitsSpace.simpleRoot_homogeneous line 819
  85. theorem OAI.KLInvariance.TitsSpace.coefficientAction_homogeneous line 824
  86. def OAI.KLInvariance.Graded.basisPiece line 853
  87. theorem OAI.KLInvariance.Graded.mem_basisPiece line 857
  88. instance OAI.KLInvariance.Graded.basisPiece_decomposition line 860
  89. instance OAI.KLInvariance.Graded.basisPiece_graded line 876
  90. theorem OAI.KLInvariance.Graded.basis_mem_piece line 886
  91. theorem OAI.KLInvariance.Graded.pairing_homogeneous line 898
  92. def OAI.KLInvariance.TitsSpace.BottIndex line 947
  93. instance OAI.KLInvariance.TitsSpace.bottIndex_fintype line 951
  94. def OAI.KLInvariance.TitsSpace.bottDegree line 957
  95. theorem OAI.KLInvariance.TitsSpace.bottDegree_nonneg line 962
  96. def OAI.KLInvariance.TitsSpace.bottBasis line 967
  97. theorem OAI.KLInvariance.TitsSpace.bottBasis_pairing_homogeneous line 979
  98. instance OAI.KLInvariance.TitsSpace.bottRealModule line 1007
  99. instance OAI.KLInvariance.TitsSpace.bottRealTower line 1010
  100. def OAI.KLInvariance.TitsSpace.bottPiece line 1014
  101. instance OAI.KLInvariance.TitsSpace.bottPiece_decomposition line 1017
  102. instance OAI.KLInvariance.TitsSpace.bottPiece_graded line 1020
  103. theorem OAI.KLInvariance.TitsSpace.bottDuality_homogeneous line 1024
  104. theorem OAI.KLInvariance.TitsSpace.coefficientAction_one line 1050
  105. def OAI.KLInvariance.TitsSpace.bottWeight line 1056
  106. def OAI.KLInvariance.TitsSpace.weightFunctional line 1062
  107. def OAI.KLInvariance.TitsSpace.inducedFunctional line 1078
  108. def OAI.KLInvariance.TitsSpace.bottEvaluation line 1085
  109. theorem OAI.KLInvariance.TitsSpace.bottEvaluation_tmul line 1091
  110. theorem OAI.KLInvariance.TitsSpace.bottEvaluation_right line 1097
  111. def OAI.KLInvariance.ReflectionFrobenius.wallCoordinate line 1137
  112. def OAI.KLInvariance.ReflectionFrobenius.wallMatrix line 1141
  113. theorem OAI.KLInvariance.ReflectionFrobenius.wallMatrix_mulVec line 1146
  114. theorem OAI.KLInvariance.ReflectionFrobenius.matrixTwist_injective line 1158
  115. theorem OAI.KLInvariance.ReflectionFrobenius.wallCoordinate_injective line 1170
  116. def OAI.KLInvariance.TitsSpace.bottEvaluationMatrix line 1213
  117. theorem OAI.KLInvariance.TitsSpace.bottEvaluation_expand line 1216
  118. theorem OAI.KLInvariance.TitsSpace.bottEvaluationMatrix_cons line 1225
  119. theorem OAI.KLInvariance.TitsSpace.bottEvaluationMatrix_mulVec_cons line 1247
  120. theorem OAI.KLInvariance.TitsSpace.bottEvaluationMatrix_injective line 1263
  121. theorem OAI.KLInvariance.TitsSpace.bottEvaluation_injective line 1290
  122. def OAI.KLInvariance.TitsSpace.bottCoordinateDenominator line 1317
  123. theorem OAI.KLInvariance.TitsSpace.bottCoordinateDenominator_ne_zero line 1321
  124. theorem OAI.KLInvariance.TitsSpace.bottEvaluation_contains_scaled_coordinates line 1328
  125. theorem OAI.KLInvariance.TitsSpace.symmetricCoefficient_ι_injective line 1356
  126. theorem OAI.KLInvariance.TitsSpace.coefficientAction_injective line 1367
  127. theorem OAI.KLInvariance.TitsSpace.coefficientAction_separates line 1377
  128. def OAI.KLInvariance.TitsSpace.bottWeightSupported line 1403
  129. theorem OAI.KLInvariance.TitsSpace.bott_weight_eigen line 1410
  130. theorem OAI.KLInvariance.TitsSpace.bott_eigen_supported line 1423
  131. theorem OAI.KLInvariance.TitsSpace.bott_distinct_weight_orthogonal line 1437
  132. def OAI.KLInvariance.TitsSpace.bottCoordinateLift line 1448
  133. theorem OAI.KLInvariance.TitsSpace.bottCoordinateLift_eval line 1452
  134. theorem OAI.KLInvariance.TitsSpace.bottCoordinateLift_supported line 1458
  135. theorem OAI.KLInvariance.TitsSpace.bottCoordinateExpansion line 1465
  136. def OAI.KLInvariance.TitsSpace.bottWeightProjection line 1497
  137. theorem OAI.KLInvariance.TitsSpace.bottWeightProjection_eq_zero line 1502
  138. theorem OAI.KLInvariance.TitsSpace.bott_supported_annihilates line 1511
  139. theorem OAI.KLInvariance.TitsSpace.bott_annihilates_supported line 1529
  140. theorem OAI.KLInvariance.TitsSpace.bott_supported_iff_annihilates line 1553
  141. def OAI.KLInvariance.TitsSpace.bottStalk line 1558
  142. def OAI.KLInvariance.TitsSpace.bottStalkProjection line 1562
  143. theorem OAI.KLInvariance.TitsSpace.bottStalkProjection_surjective line 1566
  144. theorem OAI.KLInvariance.TitsSpace.bottStalkProjection_eq_zero line 1571
  145. def OAI.KLInvariance.TitsSpace.bottStalkDualToSupport line 1575
  146. theorem OAI.KLInvariance.TitsSpace.bottStalkDualToSupport_bijective line 1588
  147. def OAI.KLInvariance.TitsSpace.bottStalkDuality line 1610
  148. theorem OAI.KLInvariance.TitsSpace.coefficientAction_reflection line 1632
  149. theorem OAI.KLInvariance.TitsSpace.reflectionCoefficient_anti line 1638
  150. theorem OAI.KLInvariance.TitsSpace.reflectionCoefficient_divisible line 1644
  151. theorem OAI.KLInvariance.TitsSpace.reflectionCoefficient_difference line 1650
  152. def OAI.KLInvariance.TitsSpace.bottSubword line 1678
  153. theorem OAI.KLInvariance.TitsSpace.bottSubword_sublist line 1682
  154. theorem OAI.KLInvariance.TitsSpace.bottSubword_wordProd line 1693
  155. theorem OAI.KLInvariance.TitsSpace.exists_bottSubword line 1702
  156. theorem OAI.KLInvariance.TitsSpace.bottWeight_bruhat line 1713
  157. theorem OAI.KLInvariance.TitsSpace.exists_bottWeight line 1718
  158. theorem OAI.KLInvariance.TitsSpace.bottWeight_range line 1724
  159. theorem OAI.KLInvariance.TitsSpace.bottStalkProjection_right line 1751
  160. def OAI.KLInvariance.TitsSpace.bottProjectionSheaf line 1761
  161. def OAI.KLInvariance.TitsSpace.bottSection line 1776
  162. theorem OAI.KLInvariance.TitsSpace.bottProjectionSheaf_generated line 1792
  163. theorem OAI.KLInvariance.TitsSpace.bottProjectionSheaf_lower_surjective line 1798
  164. theorem OAI.KLInvariance.TitsSpace.bottProjectionSheaf_upper_surjective line 1802
  165. theorem OAI.KLInvariance.TitsSpace.bottProjectionSheaf_annihilated line 1807

    Source documentation

    An actual Bruhat reflection root annihilates the integral edge quotient.

     theorem bottProjectionSheaf_annihilated (l : List I) (u b : W) (e : Edge cs u b)
    {a : I → ℝ} (ha : Represents M cs (label cs u b e) a)
    (z : (bottProjectionSheaf cs l u b).edge e) :
    SymmetricAlgebra.ι ℝ (Extended M) (embed M a) • z = 0 := by
…

    Mentions: OAI.KLInvariance.TitsSpace.Represents, OAI.KLInvariance.TitsSpace.bottProjectionSheaf, OAI.KLInvariance.TitsSpace.Extended, OAI.KLInvariance.TitsSpace.embed

  166. theorem OAI.KLInvariance.TitsSpace.bottSection_injective line 1819
  167. theorem OAI.KLInvariance.PairProjection.kernel_upper line 1848
  168. theorem OAI.KLInvariance.PairProjection.upper_kernel_of_divisibility line 1853
  169. def OAI.KLInvariance.TitsSpace.simpleFixedAction line 1885

    Source documentation

    The reflection is linear over its actual invariant subalgebra.

    def simpleFixedAction (i : I) : SymmetricCoefficient (M := M) →ₗ[simpleFixed cs i]
…

    Mentions: OAI.KLInvariance.TitsSpace.SymmetricCoefficient, OAI.KLInvariance.TitsSpace.simpleFixed

  170. def OAI.KLInvariance.TitsSpace.bottSimpleFlip line 1896

    Source documentation

    Reflect the first tensor factor. It is not asserted to be left A-linear.

    def bottSimpleFlip (i : I) (l : List I) : BottSamelsonModule cs (i::l) →ₗ[simpleFixed cs i]
    BottSamelsonModule cs (i::l) :=
…

    Mentions: OAI.KLInvariance.TitsSpace.BottSamelsonModule, OAI.KLInvariance.TitsSpace.simpleFixed

  171. theorem OAI.KLInvariance.TitsSpace.bottSimpleFlip_tmul line 1901
  172. theorem OAI.KLInvariance.TitsSpace.bottSimpleFlip_divisible line 1907

    Source documentation

    The integral divisibility statement, before any localization.

    theorem bottSimpleFlip_divisible (i : I) (l : List I) (m : BottSamelsonModule cs (i::l)) :
    ∃ n : BottSamelsonModule cs (i::l),
      m-bottSimpleFlip cs i l m = simpleRootPolynomial (M := M) i • n := by
…

    Mentions: OAI.KLInvariance.TitsSpace.BottSamelsonModule, OAI.KLInvariance.TitsSpace.bottSimpleFlip, OAI.KLInvariance.TitsSpace.simpleRootPolynomial

  173. def OAI.KLInvariance.TitsSpace.bottIndexFlip line 1925

    Source documentation

    Exchange the two branches of the first subexpression slot.

    def bottIndexFlip (i : I) (l : List I) (e : BottIndex (i::l)) : BottIndex (i::l) :=
…

    Mentions: OAI.KLInvariance.TitsSpace.BottIndex

  174. theorem OAI.KLInvariance.TitsSpace.bottWeight_flip line 1929
  175. theorem OAI.KLInvariance.TitsSpace.bottEvaluation_flip line 1934
  176. theorem OAI.KLInvariance.TitsSpace.bottStalkProjection_flip_zero line 1954
  177. theorem OAI.KLInvariance.TitsSpace.bottSimpleWall_kernel_projection line 1968

    Source documentation

    The reverse inclusion to edge annihilation for the simple wall at the first tensor letter, expressed directly on kernel projections.

    theorem bottSimpleWall_kernel_projection (i : I) (l : List I) (x : W)
    {m : BottSamelsonModule cs (i::l)} (hm : bottStalkProjection cs (i::l) x m=0) :
    ∃ n : bottStalk cs (i::l) (cs.simple i*x),
      bottStalkProjection cs (i::l) (cs.simple i*x) m = simpleRootPolynomial (M := M) i • n := by
…

    Mentions: OAI.KLInvariance.TitsSpace.BottSamelsonModule, OAI.KLInvariance.TitsSpace.bottStalkProjection, OAI.KLInvariance.TitsSpace.bottStalk, OAI.KLInvariance.TitsSpace.simpleRootPolynomial

  178. theorem OAI.KLInvariance.TitsSpace.simpleCoefficient_difference line 1978
  179. theorem OAI.KLInvariance.TitsSpace.bottSimpleEdge_annihilated line 1991

    Source documentation

    Any old word's simple-edge quotient is killed by the actual label.

    theorem bottSimpleEdge_annihilated (i : I) (l : List I) (x : W)
    (z : PairProjection.Edge (bottStalkProjection cs l x)
      (bottStalkProjection cs l (cs.simple i*x))) :
    simpleRootPolynomial (M := M) i • z = 0 := by
…

    Mentions: OAI.KLInvariance.PairProjection.Edge, OAI.KLInvariance.TitsSpace.bottStalkProjection, OAI.KLInvariance.TitsSpace.simpleRootPolynomial

  180. theorem OAI.KLInvariance.TitsSpace.bottSimpleEdge_kernel_inclusion line 2002
  181. theorem OAI.KLInvariance.TitsSpace.bottSimpleWall_annihilated line 2011

    Source documentation

    The integral edge quotient is killed by its actual simple-root label.

    theorem bottSimpleWall_annihilated (i : I) (l : List I) (x : W)
    (z : PairProjection.Edge (bottStalkProjection cs (i::l) x)
      (bottStalkProjection cs (i::l) (cs.simple i*x))) :
    simpleRootPolynomial (M := M) i • z = 0 :=
…

    Mentions: OAI.KLInvariance.PairProjection.Edge, OAI.KLInvariance.TitsSpace.bottStalkProjection, OAI.KLInvariance.TitsSpace.simpleRootPolynomial

  182. theorem OAI.KLInvariance.TitsSpace.bottSimpleWall_upper_kernel line 2018

    Source documentation

    The exact integral quotient kernel, without a free-stalk hypothesis.

    theorem bottSimpleWall_upper_kernel (i : I) (l : List I) (x : W)
    (z : bottStalk cs (i::l) (cs.simple i*x)) :
    PairProjection.upper (bottStalkProjection cs (i::l) x)
      (bottStalkProjection cs (i::l) (cs.simple i*x)) z = 0 ↔
    ∃ n : bottStalk cs (i::l) (cs.simple i*x), z = simpleRootPolynomial (M := M) i • n :=
…

    Mentions: OAI.KLInvariance.TitsSpace.bottStalk, OAI.KLInvariance.PairProjection.upper, OAI.KLInvariance.TitsSpace.bottStalkProjection, OAI.KLInvariance.TitsSpace.simpleRootPolynomial

  183. structure OAI.KLInvariance.ReflectionPairTranslation.Twist line 2045

    Source documentation

    Restriction of the scalar action along a ring automorphism.

    @[ext] structure Twist (_τ : R ≃+* R) (Y : Type z) where
…
  184. def OAI.KLInvariance.ReflectionPairTranslation.Twist.equivVal line 2053
  185. instance OAI.KLInvariance.ReflectionPairTranslation.Twist.(instance at line 2058) line 2058
  186. instance OAI.KLInvariance.ReflectionPairTranslation.Twist.(instance at line 2059) line 2059
  187. def OAI.KLInvariance.ReflectionPairTranslation.Twist.equiv line 2063
  188. instance OAI.KLInvariance.ReflectionPairTranslation.Twist.(instance at line 2073) line 2073
  189. def OAI.KLInvariance.ReflectionPairTranslation.lattice line 2086

    Source documentation

    The old pair relation with the scalar action on its second factor twisted. Alpha-annihilation of the old edge is what makes this an R-submodule.

    def lattice : Submodule R (X × Twist τ Y) where
…

    Mentions: OAI.KLInvariance.ReflectionPairTranslation.Twist

  190. theorem OAI.KLInvariance.ReflectionPairTranslation.lattice_saturated line 2106

    Source documentation

    Saturation away from the simple wall. Regularity on the old edge module, not an unjustified reflexivity assertion, removes a non-wall factor.

    theorem lattice_saturated (β : R)
    (hann : ∀ e : PairProjection.Edge f g, α • e=0)
    (hreg : Function.Injective (fun e : PairProjection.Edge f g => β • e))
    (p : X × Twist τ Y) :
    β • p ∈ lattice f g τ α hdiv hinc ↔ p ∈ lattice f g τ α hdiv hinc := by
…

    Mentions: OAI.KLInvariance.PairProjection.Edge, OAI.KLInvariance.ReflectionPairTranslation.Twist, OAI.KLInvariance.ReflectionPairTranslation.lattice

  191. def OAI.KLInvariance.ReflectionPairTranslation.left line 2127

    Source documentation

    Surjective projection to the untwisted (lower) stalk.

    def left : lattice f g τ α hdiv hinc →ₗ[R] X :=
…

    Mentions: OAI.KLInvariance.ReflectionPairTranslation.lattice

  192. theorem OAI.KLInvariance.ReflectionPairTranslation.left_surjective line 2130
  193. def OAI.KLInvariance.ReflectionPairTranslation.kernelMap line 2137

    Source documentation

    Its kernel is the alpha-multiple of the twisted upper stalk.

    def kernelMap : Twist τ Y →ₗ[R] LinearMap.ker (left f g τ α hdiv hinc) where
…

    Mentions: OAI.KLInvariance.ReflectionPairTranslation.Twist, OAI.KLInvariance.ReflectionPairTranslation.left

  194. theorem OAI.KLInvariance.ReflectionPairTranslation.kernelMap_surjective line 2155
  195. theorem OAI.KLInvariance.ReflectionPairTranslation.kernelMap_injective line 2165
  196. def OAI.KLInvariance.ReflectionPairTranslation.kernelEquiv line 2171
  197. theorem OAI.KLInvariance.ReflectionPairTranslation.free_of_surjective_of_ker_free line 2178

    Source documentation

    A split extension of free modules is free. This does not assert the false statement that every submodule of a free polynomial module is free.

    theorem free_of_surjective_of_ker_free {P : Type*} [AddCommGroup P] [Module R P]
    {Q : Type*} [AddCommGroup Q] [Module R Q]
    (π : P →ₗ[R] Q) (hπ : Function.Surjective π)
    [Module.Free R Q] [Module.Free R (LinearMap.ker π)] : Module.Free R P := by
…
  198. theorem OAI.KLInvariance.ReflectionPairTranslation.lattice_free line 2206