HopfAlgebra.tensorQuotientAlgEquiv |
def |
AlgebraicGroups/Algebra/HopfAlgebra/TensorQuotient.lean, line 571 |
|
HopfAlgebra.tensorQuotientAlgEquiv_toLinearEquiv |
theorem |
AlgebraicGroups/Algebra/HopfAlgebra/TensorQuotient.lean, line 582 |
|
HopfAlgebra.tensorQuotientEquiv |
def |
AlgebraicGroups/Algebra/HopfAlgebra/TensorQuotient.lean, line 440 |
|
HopfAlgebra.tensorQuotientEquiv_tmul |
theorem |
AlgebraicGroups/Algebra/HopfAlgebra/TensorQuotient.lean, line 461 |
|
HopfAlgebra.tensorQuotientEquiv_symm_tmul |
theorem |
AlgebraicGroups/Algebra/HopfAlgebra/TensorQuotient.lean, line 470 |
|
AlgebraicGeometry.groupSchemeClosedPoints_isClosed_iff_mem_nhdsWithin_closure |
theorem |
AlgebraicGroups/GroupScheme/ClosedPointSubgroup.lean, line 81 |
|
AlgebraicGeometry.groupSchemeClosedPoints_isClosed_of_isLocallyClosed |
theorem |
AlgebraicGroups/GroupScheme/ClosedPointSubgroup.lean, line 119 |
|
Coalgebra.comul_mem_range_mapIncl_span_of_isGroupLikeElem |
theorem |
AlgebraicGroups/Algebra/Coalgebra/GroupLikeSpan.lean, line 34 |
|
Coalgebra.span_le_span_coefficients |
theorem |
AlgebraicGroups/Algebra/Coalgebra/Coefficients.lean, line 69 |
|
Coalgebra.comul_coefficient |
theorem |
AlgebraicGroups/Algebra/Coalgebra/Coefficients.lean, line 106 |
|
Coalgebra.counit_coefficient |
theorem |
AlgebraicGroups/Algebra/Coalgebra/Coefficients.lean, line 118 |
|
Coalgebra.comul_mem_range_mapIncl_span_coefficients |
theorem |
AlgebraicGroups/Algebra/Coalgebra/Coefficients.lean, line 131 |
|
Coalgebra.exists_fg_submodule_comul_right_closed_of_finite |
theorem |
AlgebraicGroups/Algebra/Coalgebra/FiniteSubcoalgebra.lean, line 234 |
|
Coalgebra.exists_basis_comul_coefficients |
theorem |
AlgebraicGroups/Algebra/Coalgebra/FiniteSubcoalgebra.lean, line 252 |
|
Coalgebra.exists_fg_submodule_comul_closed_of_finite |
theorem |
AlgebraicGroups/Algebra/Coalgebra/FiniteSubcoalgebra.lean, line 297 |
|
HopfAlgebra.coefficientMatrix_mul_antipode |
theorem |
AlgebraicGroups/Algebra/Coalgebra/CoefficientMatrixUnit.lean, line 140 |
|
HopfAlgebra.antipode_mul_coefficientMatrix |
theorem |
AlgebraicGroups/Algebra/Coalgebra/CoefficientMatrixUnit.lean, line 153 |
|
HopfAlgebra.coefficientMatrixUnit |
def |
AlgebraicGroups/Algebra/Coalgebra/CoefficientMatrixUnit.lean, line 166 |
|
Coalgebra.counit_range_mul_self |
theorem |
AlgebraicGroups/Algebra/Coalgebra/CounitRange.lean, line 104 |
|
Coalgebra.counit_range_smul_top |
theorem |
AlgebraicGroups/Algebra/Coalgebra/CounitRange.lean, line 131 |
|
IsIdempotentElem.coalgebraSpan |
def |
AlgebraicGroups/Algebra/Coalgebra/IdempotentIdeal.lean, line 76 |
|
TensorProduct.equivFinsuppOfBasisRight_lTensor_apply |
theorem |
AlgebraicGroups/Algebra/TensorProduct/Split.lean, line 48 |
|
TensorProduct.sum_tmul_eq_of_split |
theorem |
AlgebraicGroups/Algebra/TensorProduct/Split.lean, line 61 |
|
TensorProduct.exists_tensor_coefficients_of_split |
theorem |
AlgebraicGroups/Algebra/TensorProduct/Split.lean, line 89 |
|
AlgebraicGeometry.affineSpecHomOverEquiv |
def |
AlgebraicGroups/GroupScheme/AffineHomOver.lean, line 47 |
|
AlgebraicGeometry.additiveGroupHomOverEquiv |
def |
AlgebraicGroups/GroupScheme/AffineHomOver.lean, line 122 |
|
AlgebraicGeometry.additiveGroupAffineProductFan_isLimit |
abbrev |
AlgebraicGroups/GroupScheme/AdditiveProductAffineSpace.lean, line 154 |
|
AlgebraicGeometry.additiveGroupProductUnderlyingSpecIso |
def |
AlgebraicGroups/GroupScheme/AdditiveProductAffineSpace.lean, line 183 |
|
AlgebraicGeometry.additiveGroupProductUnderlyingSpecIso_hom_projection |
theorem |
AlgebraicGroups/GroupScheme/AdditiveProductAffineSpace.lean, line 191 |
|
AlgebraicGeometry.additiveGroupProductUnderlyingAffineSpaceIso |
def |
AlgebraicGroups/GroupScheme/AdditiveProductAffineSpace.lean, line 212 |
|
AlgebraicGeometry.additiveGroupProductUnderlyingAffineSpaceIso_coordinate |
theorem |
AlgebraicGroups/GroupScheme/AdditiveProductAffineSpace.lean, line 221 |
|
AlgebraicGeometry.stageProductCoordinatePullback_X |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageProjectionBridge.lean, line 100 |
|
AlgebraicGeometry.unitriangularStageCoordinateMap_underlying_spec |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageProjectionBridge.lean, line 204 |
|
AlgebraicGeometry.unitriangularStageCoordinateMap_underlying_affineSpace |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageProjectionBridge.lean, line 218 |
|
AlgebraicGeometry.stageProductSectionPullback_inclusion |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageProjectionBridge.lean, line 280 |
|
AlgebraicGeometry.stageProductSectionPullback_higher |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageProjectionBridge.lean, line 296 |
|
AlgebraicGeometry.unitriangularStageCoordinateSectionOver_comp |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageProjectionBridge.lean, line 419 |
|
MvPolynomial.eraseCoordinates |
def |
AlgebraicGroups/Algebra/LocalizedCoordinateQuotient.lean, line 50 |
|
MvPolynomial.localizedCoordinateIdeal |
def |
AlgebraicGroups/Algebra/LocalizedCoordinateQuotient.lean, line 79 |
|
MvPolynomial.quotient_killed |
theorem |
AlgebraicGroups/Algebra/LocalizedCoordinateQuotient.lean, line 83 |
|
MvPolynomial.localizedCoordinateQuotientEquiv |
def |
AlgebraicGroups/Algebra/LocalizedCoordinateQuotient.lean, line 201 |
|
MvPolynomial.localizedCoordinateQuotientEquiv_algebraMap |
theorem |
AlgebraicGroups/Algebra/LocalizedCoordinateQuotient.lean, line 249 |
|
MvPolynomial.localizedCoordinateQuotientEquiv_symm_algebraMap |
theorem |
AlgebraicGroups/Algebra/LocalizedCoordinateQuotient.lean, line 259 |
|
MvPolynomial.ringKrullDim_localizationAway_of_eval_ne_zero |
theorem |
AlgebraicGroups/Algebra/FinitePolynomialLocalizationDimension.lean, line 59 |
|
DiagonalCoordinateRing.ideal_eq_localizedCoordinateIdeal |
theorem |
AlgebraicGroups/GroupScheme/DiagonalDimension.lean, line 55 |
|
DiagonalCoordinateRing.localizedPolynomialEquiv |
def |
AlgebraicGroups/GroupScheme/DiagonalDimension.lean, line 80 |
|
DiagonalCoordinateRing.localizedPolynomialEquiv_diagonal |
theorem |
AlgebraicGroups/GroupScheme/DiagonalDimension.lean, line 103 |
|
DiagonalCoordinateRing.localizedPolynomialEquiv_symm_diagonal |
theorem |
AlgebraicGroups/GroupScheme/DiagonalDimension.lean, line 114 |
|
DiagonalCoordinateRing.erasedDeterminant_eval_one |
theorem |
AlgebraicGroups/GroupScheme/DiagonalDimension.lean, line 137 |
|
AlgebraicGeometry.diagonalCoordinateRing_ringKrullDim |
theorem |
AlgebraicGroups/GroupScheme/DiagonalDimension.lean, line 178 |
|
AlgebraicGeometry.diagonalGroupUnderlyingScheme_topologicalKrullDim |
theorem |
AlgebraicGroups/GroupScheme/DiagonalDimension.lean, line 201 |
|
UnitriangularCoordinateRing.baseChange |
def |
AlgebraicGroups/Algebra/UnitriangularBaseChange.lean, line 90 |
|
UnitriangularCoordinateRing.baseChange_presentation |
theorem |
AlgebraicGroups/Algebra/UnitriangularBaseChange.lean, line 95 |
|
UnitriangularCoordinateRing.baseChange_tmul_freeEquiv |
theorem |
AlgebraicGroups/Algebra/UnitriangularBaseChange.lean, line 106 |
|
UnitriangularCoordinateRing.baseChange_tmul_one |
theorem |
AlgebraicGroups/Algebra/UnitriangularBaseChange.lean, line 112 |
|
UnitriangularCoordinateRing.baseChange_tmul_entry |
theorem |
AlgebraicGroups/Algebra/UnitriangularBaseChange.lean, line 141 |
|
UnitriangularCoordinateRing.baseChange_symm_entry |
theorem |
AlgebraicGroups/Algebra/UnitriangularBaseChange.lean, line 164 |
|
UnitriangularCoordinateRing.baseChange_symm_algebraMap |
theorem |
AlgebraicGroups/Algebra/UnitriangularBaseChange.lean, line 174 |
|
UnitriangularCoordinateRing.baseChange_self |
theorem |
AlgebraicGroups/Algebra/UnitriangularBaseChangeCoherence.lean, line 48 |
|
UnitriangularCoordinateRing.baseChange_tower |
theorem |
AlgebraicGroups/Algebra/UnitriangularBaseChangeCoherence.lean, line 68 |
|
UnitriangularCoordinateRing.ideal_isHopfIdeal |
instance |
AlgebraicGroups/Algebra/UnitriangularCoordinateRing.lean, line 249 |
|
UnitriangularCoordinateRing.coordinatePolynomialEquiv |
def |
AlgebraicGroups/Algebra/UnitriangularCoordinateRing.lean, line 443 |
|
UnitriangularCoordinateRing.polynomialFreeEquiv |
def |
AlgebraicGroups/Algebra/UnitriangularCoordinateRing.lean, line 576 |
|
UnitriangularCoordinateRing.freeEquiv |
def |
AlgebraicGroups/Algebra/UnitriangularCoordinateRing.lean, line 586 |
|
UnitriangularCoordinateRing.freeEquiv_variable |
theorem |
AlgebraicGroups/Algebra/UnitriangularCoordinateRing.lean, line 589 |
|
UnitriangularCoordinateRing.finiteType |
instance |
AlgebraicGroups/Algebra/UnitriangularCoordinateRing.lean, line 624 |
|
UnitriangularStageCoordinateRing.ideal |
def |
AlgebraicGroups/Algebra/UnitriangularStageCoordinateRing.lean, line 54 |
|
UnitriangularStageCoordinateRing.CoordinateRing |
abbrev |
AlgebraicGroups/Algebra/UnitriangularStageCoordinateRing.lean, line 60 |
|
UnitriangularStageCoordinateRing.mem_stage_iff |
theorem |
AlgebraicGroups/Algebra/UnitriangularStageCoordinateRing.lean, line 78 |
|
UnitriangularStageCoordinateRing.ideal_isHopfIdeal_proof |
theorem |
AlgebraicGroups/Algebra/UnitriangularStageCoordinateRing.lean, line 257 |
|
UnitriangularStageCoordinateRing.quotientBialgHom |
def |
AlgebraicGroups/Algebra/UnitriangularStageCoordinateRing.lean, line 274 |
|
UnitriangularStageCoordinateRing.successor |
def |
AlgebraicGroups/Algebra/UnitriangularStageCoordinateRing.lean, line 295 |
|
UnitriangularStageCoordinateRing.SurvivingPair |
abbrev |
AlgebraicGroups/Algebra/UnitriangularStagePolynomial.lean, line 41 |
|
UnitriangularStageCoordinateRing.polynomialEquiv |
def |
AlgebraicGroups/Algebra/UnitriangularStagePolynomial.lean, line 188 |
|
UnitriangularStageCoordinateRing.polynomialEquiv_surviving |
theorem |
AlgebraicGroups/Algebra/UnitriangularStagePolynomial.lean, line 202 |
|
UnitriangularStageCoordinateRing.polynomialEquiv_forbidden |
theorem |
AlgebraicGroups/Algebra/UnitriangularStagePolynomial.lean, line 208 |
|
UnitriangularStageCoordinateRing.polynomialEquiv_symm_X |
theorem |
AlgebraicGroups/Algebra/UnitriangularStagePolynomial.lean, line 215 |
|
Matrix.unitriangularSubgroup |
def |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 48 |
|
Matrix.UnitriangularGroup.map |
def |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 83 |
|
AlgebraicGeometry.unitriangularGroupScheme |
abbrev |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 129 |
|
AlgebraicGeometry.unitriangularInclusion |
def |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 139 |
|
AlgebraicGeometry.unitriangularInclusion_isClosedImmersion |
theorem |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 150 |
|
AlgebraicGeometry.unitriangularGroupMulEquivAlgHom |
def |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 219 |
|
AlgebraicGeometry.unitriangularGroupMulEquivPoints |
def |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 258 |
|
AlgebraicGeometry.unitriangularGroupPointsIso |
def |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 343 |
|
AlgebraicGeometry.unitriangularFromGL_natural |
theorem |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 302 |
|
AlgebraicGeometry.unitriangularInclusion_point |
theorem |
AlgebraicGroups/GroupScheme/Unitriangular.lean, line 278 |
|
AlgebraicGeometry.unitriangularStageScheme |
abbrev |
AlgebraicGroups/GroupScheme/UnitriangularStages.lean, line 51 |
|
AlgebraicGeometry.unitriangularStageInclusion |
def |
AlgebraicGroups/GroupScheme/UnitriangularStages.lean, line 57 |
|
AlgebraicGeometry.unitriangularStageInclusion_isClosedImmersion |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStages.lean, line 66 |
|
AlgebraicGeometry.unitriangularStageSuccessor |
def |
AlgebraicGroups/GroupScheme/UnitriangularStages.lean, line 107 |
|
AlgebraicGeometry.unitriangularStageSuccessor_isClosedImmersion |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStages.lean, line 116 |
|
AlgebraicGeometry.unitriangularStagePointMulEquiv |
def |
AlgebraicGroups/GroupScheme/UnitriangularStages.lean, line 218 |
|
AlgebraicGeometry.unitriangularStagePointsIso |
def |
AlgebraicGroups/GroupScheme/UnitriangularStages.lean, line 341 |
|
AlgebraicGeometry.unitriangularStageUnderlyingAffineSpaceIso |
def |
AlgebraicGroups/GroupScheme/UnitriangularStageAffineSpace.lean, line 46 |
|
AlgebraicGeometry.unitriangularStageUnderlyingAffineSpaceIso_preimage_variable |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageAffineSpace.lean, line 68 |
|
AlgebraicGeometry.unitriangularStageUnderlyingAffineSpaceIso_preimage_inverse |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageAffineSpace.lean, line 87 |
|
AlgebraicGeometry.unitriangularStageConjugation |
def |
AlgebraicGroups/GroupScheme/UnitriangularStageNormality.lean, line 120 |
|
AlgebraicGeometry.unitriangularStageConjugation_inclusion |
theorem |
AlgebraicGroups/GroupScheme/UnitriangularStageNormality.lean, line 131 |
|
AlgebraicGeometry.unitriangularStageInclusion_normal |
instance |
AlgebraicGroups/GroupScheme/UnitriangularStageNormality.lean, line 159 |
|