Main results 101 to 149

Declaration Kind Where Note
AlgebraicGeometry.Scheme.RationalMap.functionFieldMap def SchemeProperties/RationalFunctionFieldPullback.lean, line 82
AlgebraicGeometry.Scheme.RationalMap.functionFieldMap_eq_of_fromFunctionField_eq theorem SchemeProperties/RationalFunctionFieldPullback.lean, line 97
AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_comp theorem SchemeProperties/RationalFunctionFieldPullback.lean, line 165
AlgebraicGeometry.Scheme.RationalMap.functionFieldMap_id theorem SchemeProperties/RationalFunctionFieldPullback.lean, line 197
AlgebraicGeometry.Scheme.RationalMap.functionFieldMap_comp theorem SchemeProperties/RationalFunctionFieldPullback.lean, line 177
AlgebraicGeometry.IntegralDominantRationalScheme.functionFieldFunctor def SchemeProperties/RationalFunctionFieldPullback.lean, line 218
AlgebraicGeometry.Scheme.RationalMap.eq_of_functionFieldMap_eq theorem SchemeProperties/RationalFunctionFieldFaithfulness.lean, line 57
AlgebraicGeometry.Scheme.RationalMap.ofFunctionFieldMap def SchemeProperties/RationalFunctionFieldReconstruction.lean, line 47
AlgebraicGeometry.Scheme.RationalMap.ofFunctionFieldMap_compHom theorem SchemeProperties/RationalFunctionFieldReconstruction.lean, line 54
AlgebraicGeometry.Scheme.RationalMap.isDominant_ofFunctionFieldMap theorem SchemeProperties/RationalFunctionFieldReconstruction.lean, line 84
AlgebraicGeometry.Scheme.RationalMap.ofFunctionFieldMap_isDominant instance SchemeProperties/RationalFunctionFieldReconstruction.lean, line 136
AlgebraicGeometry.Scheme.RationalMap.functionFieldMap_ofFunctionFieldMap theorem SchemeProperties/RationalFunctionFieldReconstruction.lean, line 144
AlgebraicGeometry.Scheme.RationalMap.functionFieldMap_compatible theorem SchemeProperties/RationalFunctionFieldReconstruction.lean, line 161
AlgebraicGeometry.Scheme.RationalMap.ofFunctionFieldMap_functionFieldMap theorem SchemeProperties/RationalFunctionFieldReconstruction.lean, line 179
AlgebraicGeometry.IntegralDominantRationalSchemeOver.isIso_functionFieldMap theorem SchemeProperties/RationalFunctionFieldInverse.lean, line 82
AlgebraicGeometry.IntegralDominantRationalSchemeOver.isIso_iff_isIso_functionFieldMap theorem SchemeProperties/RationalFunctionFieldInverse.lean, line 112
AlgebraicGeometry.Scheme.RationalMap.exists_partialIso_of_inverse theorem SchemeProperties/RationalMapPartialIso.lean, line 248
AlgebraicGeometry.Scheme.RationalMap.exists_partialIso_of_inverse_over theorem SchemeProperties/RationalMapPartialIso.lean, line 267
AlgebraicGeometry.Scheme.PartialIso.toRationalMap_isDominant instance SchemeProperties/RationalMapPartialIso.lean, line 370
AlgebraicGeometry.Scheme.PartialIso.toRationalMap_comp_symm theorem SchemeProperties/RationalMapPartialIso.lean, line 375
AlgebraicGeometry.Scheme.PartialIso.symm_toRationalMap_comp theorem SchemeProperties/RationalMapPartialIso.lean, line 384
AlgebraicGeometry.Scheme.PartialIso.toRationalMap_compHom_of_isOver theorem SchemeProperties/RationalMapPartialIso.lean, line 398
AlgebraicGeometry.Scheme.PartialIso.symm_toRationalMap_compHom_of_isOver theorem SchemeProperties/RationalMapPartialIso.lean, line 408
AlgebraicGeometry.Scheme.PartialIso.subsingleton_target theorem SchemeProperties/JacobsonBirationalObstruction.lean, line 33
AlgebraicGeometry.Scheme.not_birational_of_subsingleton_of_jacobson theorem SchemeProperties/JacobsonBirationalObstruction.lean, line 53
AlgebraicGeometry.Scheme.nontrivial_spec_polynomial theorem SchemeProperties/JacobsonBirationalObstruction.lean, line 59
AlgebraicGeometry.Scheme.not_birational_spec_field_spec_polynomial theorem SchemeProperties/JacobsonBirationalObstruction.lean, line 69
AlgebraicGeometry.Scheme.fromSpecStalk_genericPoint_isDominant instance SchemeProperties/GenericPointFunctionField.lean, line 46
AlgebraicGeometry.Scheme.fromSpecStalk_genericPoint_toRationalMap_isDominant instance SchemeProperties/GenericPointFunctionField.lean, line 55
AlgebraicGeometry.Scheme.genericPoint_functionFieldMap_specMap theorem SchemeProperties/GenericPointFunctionField.lean, line 62
AlgebraicGeometry.Scheme.genericPoint_functionFieldMap_isIso instance SchemeProperties/GenericPointFunctionField.lean, line 81
AlgebraicGeometry.Scheme.not_locallyOfFiniteType_fromSpecStalk_genericPoint theorem SchemeProperties/GenericPointFunctionField.lean, line 106
AlgebraicGeometry.Scheme.not_locallyOfFiniteType_fromSpecStalk_genericPoint_comp theorem SchemeProperties/GenericPointFunctionField.lean, line 127
AlgebraicGeometry.Scheme.RationalMap.not_twoSidedInverse_of_subsingleton_of_jacobson theorem SchemeProperties/GenericPointRationalNoninvertibility.lean, line 35
AlgebraicGeometry.Scheme.genericPointRationalHom def SchemeProperties/GenericPointRationalNoninvertibility.lean, line 54
AlgebraicGeometry.Scheme.genericPointRationalHom_toRationalMap theorem SchemeProperties/GenericPointRationalNoninvertibility.lean, line 69
AlgebraicGeometry.Scheme.genericPointRationalHom_boundary theorem SchemeProperties/GenericPointRationalNoninvertibility.lean, line 76
AlgebraicGeometry.PullbackOpenImmersion.ker_fst_mul_ker_snd theorem SchemeProperties/PullbackOpenImmersion.lean, line 46
AlgebraicGeometry.PullbackOpenImmersion.ker_toBase theorem SchemeProperties/PullbackOpenImmersion.lean, line 65
AlgebraicGeometry.PullbackOpenImmersion.awayMap_fst_bijective theorem SchemeProperties/PullbackOpenImmersion.lean, line 104
AlgebraicGeometry.PullbackOpenImmersion.awayMap_snd_bijective theorem SchemeProperties/PullbackOpenImmersion.lean, line 135
AlgebraicGeometry.PullbackOpenImmersion.fstTarget_inf_sndTarget theorem SchemeProperties/PullbackOpenImmersion.lean, line 216
AlgebraicGeometry.PullbackOpenImmersion.fstTarget_sup_sndTarget theorem SchemeProperties/PullbackOpenImmersion.lean, line 225
AlgebraicGeometry.PullbackOpenImmersion.isOpenImmersion_fstOpenMap theorem SchemeProperties/PullbackOpenImmersion.lean, line 288
AlgebraicGeometry.PullbackOpenImmersion.isOpenImmersion_sndOpenMap theorem SchemeProperties/PullbackOpenImmersion.lean, line 348
AlgebraicGeometry.PullbackOpenImmersion.range_fstOpenMap theorem SchemeProperties/PullbackOpenImmersion.lean, line 414
AlgebraicGeometry.PullbackOpenImmersion.range_sndOpenMap theorem SchemeProperties/PullbackOpenImmersion.lean, line 448
AlgebraicGeometry.PullbackOpenImmersion.disjoint_ranges theorem SchemeProperties/PullbackOpenImmersion.lean, line 482
AlgebraicGeometry.PullbackOpenImmersion.union_ranges theorem SchemeProperties/PullbackOpenImmersion.lean, line 491

Quoted from the main results in formalization.yaml of FormalFrontier/scheme-properties at commit 09db7d88, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.