Theorems · Definition · algebraic geometry
AlgebraicGeometry.AffineSpace.map
(n : Type u) →
{S T : AlgebraicGeometry.Scheme} → (S ⟶ T) → (AlgebraicGeometry.AffineSpace n S ⟶ AlgebraicGeometry.AffineSpace n T)𝔸(n; S) is functorial w.r.t. S.
- Defined in
- Mathlib.AlgebraicGeometry.AffineSpace
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.overproof · cited by 76
- AlgebraicGeometry.AffineSpacestatement and proof · cited by 51
- AlgebraicGeometry.AffineSpace.coordproof · cited by 19
- AlgebraicGeometry.AffineSpace.homOfVectorproof · cited by 9
Cited by16
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.AffineSpace.map_appTop_coordstatement · cited by 5
- AlgebraicGeometry.AffineSpace.map_overstatement · cited by 5
- AlgebraicGeometry.AffineSpace.functorproof · cited by 3
- AlgebraicGeometry.AffineSpace.isPullback_mapstatement and proof · cited by 2
- AlgebraicGeometry.AffineSpace.map_toSpecMvPolystatement and proof · cited by 2
- AlgebraicGeometry.AffineSpace.map_compstatement and proof · cited by 1
- AlgebraicGeometry.AffineSpace.map_over_assocstatement and proof · cited by 1
- AlgebraicGeometry.AffineSpace.map_reindexstatement and proof · cited by 1
- AlgebraicGeometry.AffineSpace.mapSpecMapstatement · cited by 0
- AlgebraicGeometry.AffineSpace.map_SpecMapstatement and proof · cited by 0
- AlgebraicGeometry.AffineSpace.map_comp_assocstatement and proof · cited by 0
- AlgebraicGeometry.AffineSpace.map_idstatement and proof · cited by 0