BottSamelson.lean`

GitHub source file

177 declarations, 0 contain sorry, 0 declared as axioms

Bott-Samelson tensor ranges, actual sections, grading and right kernels.

theorem OAI.KLInvariance.tensor_range_le_of_one_tmul line 18
theorem OAI.KLInvariance.tensor_maps_eq_of_one_tmul line 29
theorem OAI.KLInvariance.codRestrict_surjective_of_range_le line 40
theorem OAI.KLInvariance.TitsSpace.bottWeightProjection_range_le line 60
theorem OAI.KLInvariance.TitsSpace.bottTensor_maps_eq line 70
theorem OAI.KLInvariance.TitsSpace.bottWeight_tail_zero line 99
theorem OAI.KLInvariance.TitsSpace.bottWeight_tail_one line 105
def OAI.KLInvariance.TitsSpace.bottHeadPairCoordinates line 112
theorem OAI.KLInvariance.TitsSpace.bottHeadPairCoordinates_injective line 135
theorem OAI.KLInvariance.TitsSpace.simpleReverseDivisibility line 156
def OAI.KLInvariance.TitsSpace.bottHeadPairLattice line 162
instance OAI.KLInvariance.TitsSpace.bottHeadPairAddCommGroup line 166
instance OAI.KLInvariance.TitsSpace.bottHeadPairModule line 169
theorem OAI.KLInvariance.TitsSpace.bottHeadPairCoordinates_seed line 172
def OAI.KLInvariance.TitsSpace.bottHeadPairToStalk line 181
theorem OAI.KLInvariance.TitsSpace.bottHeadPairToStalk_injective line 192
theorem OAI.KLInvariance.TitsSpace.bottHeadPair_range line 197
theorem OAI.KLInvariance.TitsSpace.bottHeadPairToStalk_surjective line 207
def OAI.KLInvariance.TitsSpace.bottHeadPairEquiv line 214
def OAI.KLInvariance.TitsSpace.bottFullIndex line 237
theorem OAI.KLInvariance.TitsSpace.bottWeight_full line 242
theorem OAI.KLInvariance.TitsSpace.bottSubword_length_eq_full line 251
theorem OAI.KLInvariance.TitsSpace.bottWeight_eq_top line 269
def OAI.KLInvariance.TitsSpace.bottUnit line 276
theorem OAI.KLInvariance.TitsSpace.bottEvaluation_unit line 280
theorem OAI.KLInvariance.TitsSpace.bottEvaluation_surjective line 289
def OAI.KLInvariance.TitsSpace.bottTopCoordinate line 295
theorem OAI.KLInvariance.TitsSpace.bottTopCoordinate_bijective line 300
def OAI.KLInvariance.TitsSpace.bottTopStalkEquiv line 314
theorem OAI.KLInvariance.TitsSpace.bottEvaluation_basis_homogeneous line 338
theorem OAI.KLInvariance.TitsSpace.bottEvaluation_homogeneous line 367
theorem OAI.KLInvariance.TitsSpace.bottEvaluation_component line 384
theorem OAI.KLInvariance.TitsSpace.bottUnit_homogeneous line 391
def OAI.KLInvariance.TitsSpace.bottCoordinatePiece line 421
instance OAI.KLInvariance.TitsSpace.bottCoordinatePiece_decomposition line 425
instance OAI.KLInvariance.TitsSpace.bottCoordinatePiece_graded line 431
theorem OAI.KLInvariance.TitsSpace.bottWeightProjection_homogeneous line 436
theorem OAI.KLInvariance.TitsSpace.bottStalk_homogeneous line 442
def OAI.KLInvariance.TitsSpace.bottStalkPiece line 449
instance OAI.KLInvariance.TitsSpace.bottStalkPiece_decomposition line 452
instance OAI.KLInvariance.TitsSpace.bottStalkPiece_graded line 457
theorem OAI.KLInvariance.TitsSpace.bottStalkProjection_homogeneous line 462
theorem OAI.KLInvariance.TitsSpace.bottStalk_homogeneous_lift line 467
theorem OAI.KLInvariance.TitsSpace.bottWeightSupported_homogeneous line 481
def OAI.KLInvariance.TitsSpace.bottSupportPiece line 487
instance OAI.KLInvariance.TitsSpace.bottSupportPiece_decomposition line 491
instance OAI.KLInvariance.TitsSpace.bottSupportPiece_graded line 496
theorem OAI.KLInvariance.TitsSpace.bottTopStalkEquiv_homogeneous line 502
instance OAI.KLInvariance.ReflectionPairTranslation.Twist.scalarModule line 531
instance OAI.KLInvariance.ReflectionPairTranslation.Twist.scalarTower line 535
def OAI.KLInvariance.ReflectionPairTranslation.Twist.scalarEquiv line 541
theorem OAI.KLInvariance.Graded.equiv_inverse_homogeneous line 567
theorem OAI.KLInvariance.Graded.pairing_to_dual_homogeneous line 587
theorem OAI.KLInvariance.Graded.perfectPairing_inverse_homogeneous line 599
def OAI.KLInvariance.TitsSpace.bottHeadLeft line 629
def OAI.KLInvariance.TitsSpace.bottHeadRight line 636
theorem OAI.KLInvariance.TitsSpace.bottHeadLeft_surjective line 644
theorem OAI.KLInvariance.TitsSpace.bottHeadPairEquiv_coordinates line 649
theorem OAI.KLInvariance.TitsSpace.bottHeadLeft_homogeneous line 655
theorem OAI.KLInvariance.TitsSpace.bottHeadRight_homogeneous line 669
def OAI.KLInvariance.ReflectionPairTranslation.tensorFirst line 706
theorem OAI.KLInvariance.ReflectionPairTranslation.tensorFirst_tmul line 710
def OAI.KLInvariance.ReflectionPairTranslation.tensorSecond line 713
theorem OAI.KLInvariance.ReflectionPairTranslation.tensorSecond_tmul line 726
def OAI.KLInvariance.ReflectionPairTranslation.twistMap line 729
def OAI.KLInvariance.TitsSpace.bottHeadTail line 750
def OAI.KLInvariance.TitsSpace.bottHeadReflectedTail line 754
theorem OAI.KLInvariance.TitsSpace.bottHeadTail_seed line 760
theorem OAI.KLInvariance.TitsSpace.bottHeadReflectedTail_seed line 764
def OAI.KLInvariance.TitsSpace.bottHeadLocalPair line 769
theorem OAI.KLInvariance.TitsSpace.bottHeadLocalPair_seed line 777
theorem OAI.KLInvariance.linearMap_mem_of_coordinates line 798
theorem OAI.KLInvariance.TitsSpace.bottHeadLocalPair_coordinates line 820
theorem OAI.KLInvariance.TitsSpace.bottHeadLocalPair_mem line 828
theorem OAI.KLInvariance.TitsSpace.bottHeadLocalPair_zero_iff line 836
theorem OAI.KLInvariance.TitsSpace.bottHeadLocalPair_value line 853
theorem OAI.KLInvariance.TitsSpace.bottHeadLocalPair_toStalk line 859
theorem OAI.KLInvariance.TitsSpace.bottHeadStalk_divisible_of_pair line 866
theorem OAI.KLInvariance.FiniteFreeScalar.exists_smul_iff line 898
theorem OAI.KLInvariance.FiniteFreeScalar.exists_prod_smul line 912
theorem OAI.KLInvariance.FiniteFreeScalar.scalar_quotient_regular line 924
def OAI.KLInvariance.TitsSpace.BottKernelExact line 964
theorem OAI.KLInvariance.TitsSpace.simple_represents line 971
theorem OAI.KLInvariance.TitsSpace.represents_polynomial_prime line 976
theorem OAI.KLInvariance.TitsSpace.represents_polynomial_not_dvd line 982
theorem OAI.KLInvariance.TitsSpace.bottStalk_smul_injective line 992
instance OAI.KLInvariance.TitsSpace.bottStalkFinite line 997
theorem OAI.KLInvariance.TitsSpace.bottReflectionEdge_annihilated line 1001
theorem OAI.KLInvariance.TitsSpace.BottKernelExact.upper_kernel line 1012
theorem OAI.KLInvariance.TitsSpace.BottKernelExact.kernel_iff line 1020
theorem OAI.KLInvariance.TitsSpace.BottKernelExact.kernel_iff_of_mul line 1028
theorem OAI.KLInvariance.TitsSpace.BottKernelExact.projection_of_mul line 1036
theorem OAI.KLInvariance.TitsSpace.bottSimpleEdge_regular line 1060
theorem OAI.KLInvariance.TitsSpace.bottHeadPairLattice_saturated line 1088
theorem OAI.KLInvariance.TitsSpace.bottHeadStalk_divisible line 1116
theorem OAI.KLInvariance.TitsSpace.bottKernelExact_cons_nonhead line 1130
theorem OAI.KLInvariance.TitsSpace.bottKernelExact_cons line 1168
def OAI.KLInvariance.ReflectionPairTranslation.right line 1212
theorem OAI.KLInvariance.ReflectionPairTranslation.right_surjective line 1215
def OAI.KLInvariance.ReflectionPairTranslation.rightKernelMap line 1221
theorem OAI.KLInvariance.ReflectionPairTranslation.rightKernelMap_surjective line 1238
theorem OAI.KLInvariance.ReflectionPairTranslation.rightKernelMap_injective line 1248
def OAI.KLInvariance.ReflectionPairTranslation.rightKernelEquiv line 1253
theorem OAI.KLInvariance.ReflectionPairTranslation.lattice_free_right line 1260
theorem OAI.KLInvariance.TitsSpace.bottStalk_free_cons line 1282
theorem OAI.KLInvariance.TitsSpace.bottStalk_nil_subsingleton line 1311
theorem OAI.KLInvariance.TitsSpace.bottStalk_nil_free line 1318
theorem OAI.KLInvariance.TitsSpace.bottKernelExact_nil line 1326
theorem OAI.KLInvariance.Graded.ModuleData.pairLower_kernel_homogeneous line 1354
def OAI.KLInvariance.Graded.ModuleData.pairEdgePiece line 1363
def OAI.KLInvariance.Graded.ModuleData.pairEdge line 1366
def OAI.KLInvariance.Graded.ModuleData.pairLower line 1382
theorem OAI.KLInvariance.Graded.ModuleData.Hom.homogeneous_lift line 1386
def OAI.KLInvariance.Graded.ModuleData.pairUpper line 1393
theorem OAI.KLInvariance.TitsSpace.bottStalkPiece_negative line 1421
def OAI.KLInvariance.TitsSpace.bottStalkData line 1427
theorem OAI.KLInvariance.TitsSpace.bottPiece_negative line 1438
def OAI.KLInvariance.TitsSpace.bottWordData line 1449
def OAI.KLInvariance.TitsSpace.bottStalkHom line 1459
theorem OAI.KLInvariance.TitsSpace.bottStalkHom_surjective line 1464
def OAI.KLInvariance.TitsSpace.bottEdgeData line 1468
def OAI.KLInvariance.TitsSpace.bottLowerHom line 1472
def OAI.KLInvariance.TitsSpace.bottUpperHom line 1477
def OAI.KLInvariance.TitsSpace.bottGradedProjectionSheaf line 1482
theorem OAI.KLInvariance.TitsSpace.bottGradedProjectionSheaf_forget line 1489
theorem OAI.KLInvariance.TitsSpace.bottStandardStalks line 1510
theorem OAI.KLInvariance.TitsSpace.bottKernelExact line 1518
instance OAI.KLInvariance.TitsSpace.bottStalkFree line 1520
theorem OAI.KLInvariance.TitsSpace.bottProjectionSheaf_upper_kernel line 1524
def OAI.KLInvariance.kernelSourceEquiv line 1551
def OAI.KLInvariance.TitsSpace.bottHeadKernelEquiv line 1578
theorem OAI.KLInvariance.TitsSpace.bottHeadKernelEquiv_eval line 1589
def OAI.KLInvariance.TitsSpace.bottHeadKernelPiece line 1597
theorem OAI.KLInvariance.TitsSpace.bottHeadLeft_kernel_homogeneous line 1601
instance OAI.KLInvariance.TitsSpace.bottHeadKernelPiece_decomposition line 1613
theorem OAI.KLInvariance.TitsSpace.bottHeadKernelEquiv_homogeneous line 1618
def OAI.KLInvariance.Graded.homogeneousPieceEquiv line 1654
theorem OAI.KLInvariance.Graded.finrank_homogeneousEquiv line 1665
instance OAI.KLInvariance.Graded.subPiece_finite line 1686
instance OAI.KLInvariance.Graded.piPiece_finite line 1701
instance OAI.KLInvariance.TitsSpace.symmetricGrading_finite line 1731
instance OAI.KLInvariance.TitsSpace.bottCoordinatePiece_finite line 1735
instance OAI.KLInvariance.TitsSpace.bottStalkPiece_finite line 1740
theorem OAI.KLInvariance.TitsSpace.bottStalk_finrank_ascent line 1744
structure OAI.KLInvariance.CoefficientChange line 1777
def OAI.KLInvariance.CoefficientChange.equivVal line 1784
instance OAI.KLInvariance.CoefficientChange.(instance at line 1790) line 1790
instance OAI.KLInvariance.CoefficientChange.(instance at line 1791) line 1791
instance OAI.KLInvariance.CoefficientChange.(instance at line 1794) line 1794
instance OAI.KLInvariance.CoefficientChange.(instance at line 1796) line 1796
def OAI.KLInvariance.CoefficientChange.equiv line 1805
def OAI.KLInvariance.CoefficientChange.kEquiv line 1815
instance OAI.KLInvariance.CoefficientChange.(instance at line 1823) line 1823
instance OAI.KLInvariance.CoefficientChange.(instance at line 1825) line 1825
def OAI.KLInvariance.CoefficientChange.map line 1829
theorem OAI.KLInvariance.CoefficientChange.map_injective line 1835
theorem OAI.KLInvariance.CoefficientChange.map_surjective line 1838
def OAI.KLInvariance.Graded.ModuleData.changePiece line 1861
theorem OAI.KLInvariance.Graded.ModuleData.mem_changePiece line 1864
def OAI.KLInvariance.Graded.ModuleData.change line 1873
def OAI.KLInvariance.Graded.ModuleData.changeHom line 1896
theorem OAI.KLInvariance.Graded.ModuleData.change_free line 1902
def OAI.KLInvariance.TitsSpace.bottPolynomialStalkData line 1924
instance OAI.KLInvariance.TitsSpace.bottPolynomialStalkFree line 1929
def OAI.KLInvariance.TitsSpace.bottStalkCharacter line 1934
theorem OAI.KLInvariance.TitsSpace.bottPolynomialStalk_finrank line 1938
theorem OAI.KLInvariance.TitsSpace.bottStalkCharacter_hasSum line 1945
def OAI.KLInvariance.kernelTargetEquiv line 1971
def OAI.KLInvariance.kernelMixedEquiv line 1999
theorem OAI.KLInvariance.TitsSpace.bottHeadRight_surjective line 2031
theorem OAI.KLInvariance.TitsSpace.bottDescentKernel line 2037
def OAI.KLInvariance.TitsSpace.bottHeadRightKernelEquiv line 2045
theorem OAI.KLInvariance.TitsSpace.bottHeadRightKernelEquiv_eval line 2056
def OAI.KLInvariance.TitsSpace.bottHeadRightKernelPiece line 2067
theorem OAI.KLInvariance.TitsSpace.bottHeadRight_kernel_homogeneous line 2071
instance OAI.KLInvariance.TitsSpace.bottHeadRightKernelPiece_decomposition line 2079
theorem OAI.KLInvariance.TitsSpace.bottHeadRightKernelEquiv_homogeneous line 2084