Functoriality of the projective bundle of a module

The morphisms affineProjectiveBundle.map φ f : P(N) ⟶ P(M) induced by semilinear maps are functorial: the identity induces the identity (affineProjectiveBundle.map_eq_id) and composites induce composites (affineProjectiveBundle.map_eq_comp), from Mathlib's Proj.map_id and Proj.map_comp and the corresponding identities of graded maps of symmetric algebras, checked on the generators ι(M) and the constants (SymmetricAlgebra.ringHom_ext).

theorem SymmetricAlgebra.gradedMap_eq_id {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (hf : ∀ (x : M), f x = x) : gradedMap (RingHom.id R) f = GradedRingHom.id (grading R M)

The identity induces the identity graded map.

theorem SymmetricAlgebra.gradedMap_eq_comp {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S N : Type u} [CommRing S] [AddCommGroup N] [Module S N] {T P : Type u} [CommRing T] [AddCommGroup P] [Module T P] (φ : R →+* S) (ψ : S →+* T) (f : M →ₛₗ[φ] N) (g : N →ₛₗ[ψ] P) (k : M →ₛₗ[ψ.comp φ] P) (hk : ∀ (x : M), k x = g (f x)) : gradedMap (ψ.comp φ) k = (gradedMap ψ g).comp (gradedMap φ f)

Composites induce composite graded maps.

theorem AlgebraicGeometry.affineProjectiveBundle.map_eq_id {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {φ : R →+* R} (hφ : φ = RingHom.id R) (f : M →ₛₗ[φ] M) (hf : ∀ (x : M), f x = x) (hspan : Submodule.span R (Set.range ⇑f) = ⊤) : map φ f hspan = CategoryTheory.CategoryStruct.id (affineProjectiveBundle R M)

Functoriality, identity: a ring map equal to the identity and a semilinear map that is the identity on elements induce the identity of P(M).

theorem AlgebraicGeometry.affineProjectiveBundle.map_eq_comp {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S N : Type u} [CommRing S] [AddCommGroup N] [Module S N] {T P : Type u} [CommRing T] [AddCommGroup P] [Module T P] {φ : R →+* S} {ψ : S →+* T} {χ : R →+* T} (hχ : χ = ψ.comp φ) (f : M →ₛₗ[φ] N) (g : N →ₛₗ[ψ] P) (k : M →ₛₗ[χ] P) (hk : ∀ (x : M), k x = g (f x)) (hf : Submodule.span S (Set.range ⇑f) = ⊤) (hg : Submodule.span T (Set.range ⇑g) = ⊤) (hk' : Submodule.span T (Set.range ⇑k) = ⊤) : map χ k hk' = CategoryTheory.CategoryStruct.comp (map ψ g hg) (map φ f hf)

Functoriality, composites.

theorem AlgebraicGeometry.affineProjectiveBundle.map_π {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {S N : Type u} [CommRing S] [AddCommGroup N] [Module S N] (φ : R →+* S) (f : M →ₛₗ[φ] N) (hspan : Submodule.span S (Set.range ⇑f) = ⊤) : CategoryTheory.CategoryStruct.comp (map φ f hspan) (π R M) = CategoryTheory.CategoryStruct.comp (π S N) (Spec.map (CommRingCat.ofHom φ))

The base-change square commutes.

The same statements for morphisms of CommRingCat

theorem AlgebraicGeometry.affineProjectiveBundle.mapHom_eq_id {R' : CommRingCat} {M' : Type u} [AddCommGroup M'] [Module (↑R') M'] {φ : R' ⟶ R'} (hφ : φ = CategoryTheory.CategoryStruct.id R') (f : M' →ₛₗ[CommRingCat.Hom.hom φ] M') (hf : ∀ (x : M'), f x = x) (hspan : Submodule.span (↑R') (Set.range ⇑f) = ⊤) : mapHom φ f hspan = CategoryTheory.CategoryStruct.id (affineProjectiveBundle (↑R') M')

theorem AlgebraicGeometry.affineProjectiveBundle.mapHom_eq_comp {R' S' T' : CommRingCat} {M' N' P' : Type u} [AddCommGroup M'] [Module (↑R') M'] [AddCommGroup N'] [Module (↑S') N'] [AddCommGroup P'] [Module (↑T') P'] {φ : R' ⟶ S'} {ψ : S' ⟶ T'} {χ : R' ⟶ T'} (hχ : χ = CategoryTheory.CategoryStruct.comp φ ψ) (f : M' →ₛₗ[CommRingCat.Hom.hom φ] N') (g : N' →ₛₗ[CommRingCat.Hom.hom ψ] P') (k : M' →ₛₗ[CommRingCat.Hom.hom χ] P') (hk : ∀ (x : M'), k x = g (f x)) (hf : Submodule.span (↑S') (Set.range ⇑f) = ⊤) (hg : Submodule.span (↑T') (Set.range ⇑g) = ⊤) (hk' : Submodule.span (↑T') (Set.range ⇑k) = ⊤) : mapHom χ k hk' = CategoryTheory.CategoryStruct.comp (mapHom ψ g hg) (mapHom φ f hf)

theorem AlgebraicGeometry.affineProjectiveBundle.mapHom_π {R' S' : CommRingCat} {M' N' : Type u} [AddCommGroup M'] [Module (↑R') M'] [AddCommGroup N'] [Module (↑S') N'] (φ : R' ⟶ S') (f : M' →ₛₗ[CommRingCat.Hom.hom φ] N') (hspan : Submodule.span (↑S') (Set.range ⇑f) = ⊤) : CategoryTheory.CategoryStruct.comp (mapHom φ f hspan) (π (↑R') M') = CategoryTheory.CategoryStruct.comp (π (↑S') N') (Spec.map φ)

Over the base, for a morphism of CommRingCat: mapHom φ f lies over Spec.map φ.

theorem AlgebraicGeometry.affineProjectiveBundle.mapHom_π_assoc {R' S' : CommRingCat} {M' N' : Type u} [AddCommGroup M'] [Module (↑R') M'] [AddCommGroup N'] [Module (↑S') N'] (φ : R' ⟶ S') (f : M' →ₛₗ[CommRingCat.Hom.hom φ] N') (hspan : Submodule.span (↑S') (Set.range ⇑f) = ⊤) {Z : Scheme} (h : Spec ↧↑R' ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapHom φ f hspan) (CategoryTheory.CategoryStruct.comp (π (↑R') M') h) = CategoryTheory.CategoryStruct.comp (π (↑S') N') (CategoryTheory.CategoryStruct.comp (Spec.map φ) h)

Over the base, for a morphism of CommRingCat: mapHom φ f lies over Spec.map φ.