Documentation

TauCeti.AlgebraicGeometry.Fibers

Generic and special fibres #

For a scheme over a ring R, this file defines its scalar-extension fibre along a ring map R → K. For a local ring, it also defines the special fibre obtained by base change to the residue field. The projection identities and pullback witnesses expose the defining squares.

When R is a discrete valuation ring and K is a fraction ring, the generic fibre is an open subscheme of the total space. The special fibre over any local ring is a closed subscheme.

For a domain, the generic fibre is canonically isomorphic to Mathlib's scheme-theoretic fibre at the generic point. Iterated scalar extension is also canonically isomorphic to direct scalar extension, compatibly with both pullback projections.

source
@[reducible, inline]
noncomputable abbrev TauCeti.genericFiber (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)

The scalar extension of a scheme over R to a ring K, regarded as a scheme over K. When K is a fraction field of R, this is the generic fibre.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev TauCeti.genericFiberι (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
    (genericFiber R K toBase).left ⟶ X

    The canonical morphism from the scalar-extended fibre to the original total space.

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev TauCeti.specialFiber (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
      CategoryTheory.Over (AlgebraicGeometry.Spec ↧(IsLocalRing.ResidueField R))

      The special fibre of a scheme over a local ring, as a scheme over the residue field.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev TauCeti.specialFiberι (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
        (specialFiber R toBase).left ⟶ X

        The canonical morphism from the special fibre to the total space.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.genericFiber_hom (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
          (genericFiber R K toBase).hom = CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))

          The structure morphism of the generic fibre is the second projection of its defining pullback square.

          source
          @[simp]
          theorem TauCeti.specialFiber_hom (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
          (specialFiber R toBase).hom = CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (IsLocalRing.ResidueField R))))

          The structure morphism of the special fibre is the second projection of its defining pullback square.

          source
          @[simp]
          theorem TauCeti.genericFiberι_toBase (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
          CategoryTheory.CategoryStruct.comp (genericFiberι R K toBase) toBase = CategoryTheory.CategoryStruct.comp (genericFiber R K toBase).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))

          The generic-fibre projections satisfy their defining commutativity identity.

          source
          @[simp]
          theorem TauCeti.genericFiberι_toBase_assoc (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (genericFiberι R K toBase) (CategoryTheory.CategoryStruct.comp toBase h) = CategoryTheory.CategoryStruct.comp (genericFiber R K toBase).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) h)

          The generic-fibre projections satisfy their defining commutativity identity.

          source
          @[simp]
          theorem TauCeti.specialFiberι_toBase (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
          CategoryTheory.CategoryStruct.comp (specialFiberι R toBase) toBase = CategoryTheory.CategoryStruct.comp (specialFiber R toBase).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (IsLocalRing.ResidueField R))))

          The special-fibre projections satisfy their defining commutativity identity.

          source
          @[simp]
          theorem TauCeti.specialFiberι_toBase_assoc (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (specialFiberι R toBase) (CategoryTheory.CategoryStruct.comp toBase h) = CategoryTheory.CategoryStruct.comp (specialFiber R toBase).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (IsLocalRing.ResidueField R)))) h)

          The special-fibre projections satisfy their defining commutativity identity.

          source
          theorem TauCeti.isPullback_genericFiber (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
          CategoryTheory.IsPullback (genericFiberι R K toBase) (genericFiber R K toBase).hom toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))

          The square defining the generic fibre is a pullback.

          source
          theorem TauCeti.isPullback_specialFiber (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
          CategoryTheory.IsPullback (specialFiberι R toBase) (specialFiber R toBase).hom toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (IsLocalRing.ResidueField R))))

          The square defining the special fibre is a pullback.

          source
          theorem TauCeti.isOpenImmersion_Spec_map_fractionRing (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [CommRing K] [Algebra R K] [IsFractionRing R K] :
          AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))

          The morphism from the spectrum of a DVR's fraction ring is an open immersion.

          source
          theorem TauCeti.isClosedImmersion_Spec_map_residue (R : Type u) [CommRing R] [IsLocalRing R] :
          AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (IsLocalRing.ResidueField R))))

          The morphism from the spectrum of a local ring's residue field is a closed immersion.

          source
          theorem TauCeti.isOpenImmersion_genericFiberι (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [CommRing K] [Algebra R K] [IsFractionRing R K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
          AlgebraicGeometry.IsOpenImmersion (genericFiberι R K toBase)

          The generic fibre of a scheme over a discrete valuation ring is an open subscheme of the total space.

          source
          theorem TauCeti.isClosedImmersion_specialFiberι (R : Type u) [CommRing R] [IsLocalRing R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
          AlgebraicGeometry.IsClosedImmersion (specialFiberι R toBase)

          The special fibre of a scheme over a local ring is a closed subscheme of the total space.

          source
          noncomputable def TauCeti.specFractionRingIsoResidueFieldGenericPoint (R : CommRingCat) (K : Type u) [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] :
          AlgebraicGeometry.Spec ↧K ≅ AlgebraicGeometry.Spec ↧↑((AlgebraicGeometry.Spec R).residueField (genericPoint ↥(AlgebraicGeometry.Spec R)))

          The spectrum of a chosen fraction ring is isomorphic to the spectrum of the residue field at the generic point.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.specFractionRingIsoResidueFieldGenericPoint_hom_fromSpecResidueField (R : CommRingCat) (K : Type u) [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] :
            CategoryTheory.CategoryStruct.comp (specFractionRingIsoResidueFieldGenericPoint R K).hom ((AlgebraicGeometry.Spec R).fromSpecResidueField (genericPoint ↥(AlgebraicGeometry.Spec R))) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) K))

            The spectrum isomorphism from the fraction ring to the residue field at the generic point commutes with the two canonical maps to Spec R.

            source
            @[simp]
            theorem TauCeti.specFractionRingIsoResidueFieldGenericPoint_hom_fromSpecResidueField_assoc (R : CommRingCat) (K : Type u) [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec R ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (specFractionRingIsoResidueFieldGenericPoint R K).hom (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).fromSpecResidueField (genericPoint ↥(AlgebraicGeometry.Spec R))) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) K))) h

            The spectrum isomorphism from the fraction ring to the residue field at the generic point commutes with the two canonical maps to Spec R.

            source
            theorem TauCeti.isPullback_genericFiber_genericPoint {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) :
            CategoryTheory.IsPullback (genericFiberι (↑R) K toBase) (CategoryTheory.CategoryStruct.comp (genericFiber (↑R) K toBase).hom (specFractionRingIsoResidueFieldGenericPoint R K).hom) toBase ((AlgebraicGeometry.Spec R).fromSpecResidueField (genericPoint ↥(AlgebraicGeometry.Spec R)))

            After identifying the fraction ring with the residue field at the generic point, the square defining genericFiber is the square defining Mathlib's Scheme.Hom.fiber.

            source
            noncomputable def TauCeti.genericFiberIsoFiberGenericPoint {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) :
            (genericFiber (↑R) K toBase).left ≅ AlgebraicGeometry.Scheme.Hom.fiber toBase (genericPoint ↥(AlgebraicGeometry.Spec R))

            The scalar-extension generic fibre is isomorphic to Mathlib's scheme-theoretic fibre at the generic point.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem TauCeti.genericFiberIsoFiberGenericPoint_hom_fiberι {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) :
              CategoryTheory.CategoryStruct.comp (genericFiberIsoFiberGenericPoint toBase).hom (AlgebraicGeometry.Scheme.Hom.fiberι toBase (genericPoint ↥(AlgebraicGeometry.Spec R))) = genericFiberι (↑R) K toBase

              The generic-point fibre comparison commutes with the projections to the total space.

              source
              @[simp]
              theorem TauCeti.genericFiberIsoFiberGenericPoint_hom_fiberι_assoc {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (genericFiberIsoFiberGenericPoint toBase).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberι toBase (genericPoint ↥(AlgebraicGeometry.Spec R))) h) = CategoryTheory.CategoryStruct.comp (genericFiberι (↑R) K toBase) h

              The generic-point fibre comparison commutes with the projections to the total space.

              source
              @[simp]
              theorem TauCeti.genericFiberIsoFiberGenericPoint_hom_fiberToSpecResidueField {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) :
              CategoryTheory.CategoryStruct.comp (genericFiberIsoFiberGenericPoint toBase).hom (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField toBase (genericPoint ↥(AlgebraicGeometry.Spec R))) = CategoryTheory.CategoryStruct.comp (genericFiber (↑R) K toBase).hom (specFractionRingIsoResidueFieldGenericPoint R K).hom

              The generic-point fibre comparison commutes with the projections to the residue-field spectrum.

              source
              @[simp]
              theorem TauCeti.genericFiberIsoFiberGenericPoint_hom_fiberToSpecResidueField_assoc {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ((AlgebraicGeometry.Spec R).residueField (genericPoint ↥(AlgebraicGeometry.Spec R))) ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (genericFiberIsoFiberGenericPoint toBase).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField toBase (genericPoint ↥(AlgebraicGeometry.Spec R))) h) = CategoryTheory.CategoryStruct.comp (genericFiber (↑R) K toBase).hom (CategoryTheory.CategoryStruct.comp (specFractionRingIsoResidueFieldGenericPoint R K).hom h)

              The generic-point fibre comparison commutes with the projections to the residue-field spectrum.

              source
              @[simp]
              theorem TauCeti.genericFiberIsoFiberGenericPoint_inv_genericFiberι {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) :
              CategoryTheory.CategoryStruct.comp (genericFiberIsoFiberGenericPoint toBase).inv (genericFiberι (↑R) K toBase) = AlgebraicGeometry.Scheme.Hom.fiberι toBase (genericPoint ↥(AlgebraicGeometry.Spec R))

              The inverse generic-point fibre comparison commutes with the projections to the total space.

              source
              @[simp]
              theorem TauCeti.genericFiberIsoFiberGenericPoint_inv_genericFiberι_assoc {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (genericFiberIsoFiberGenericPoint toBase).inv (CategoryTheory.CategoryStruct.comp (genericFiberι (↑R) K toBase) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberι toBase (genericPoint ↥(AlgebraicGeometry.Spec R))) h

              The inverse generic-point fibre comparison commutes with the projections to the total space.

              source
              @[simp]
              theorem TauCeti.genericFiberIsoFiberGenericPoint_inv_hom {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) :
              CategoryTheory.CategoryStruct.comp (genericFiberIsoFiberGenericPoint toBase).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) K)))) (specFractionRingIsoResidueFieldGenericPoint R K).hom) = AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField toBase (genericPoint ↥(AlgebraicGeometry.Spec R))

              The inverse generic-point fibre comparison commutes with the projections to the residue-field spectrum.

              source
              @[simp]
              theorem TauCeti.genericFiberIsoFiberGenericPoint_inv_hom_assoc {R : CommRingCat} {K : Type u} [IsDomain ↑R] [CommRing K] [Algebra (↑R) K] [IsFractionRing (↑R) K] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧↑((AlgebraicGeometry.Spec R).residueField (genericPoint ↥(AlgebraicGeometry.Spec R))) ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (genericFiberIsoFiberGenericPoint toBase).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) K)))) (CategoryTheory.CategoryStruct.comp (specFractionRingIsoResidueFieldGenericPoint R K).hom h)) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField toBase (genericPoint ↥(AlgebraicGeometry.Spec R))) h

              The inverse generic-point fibre comparison commutes with the projections to the residue-field spectrum.

              source
              noncomputable def TauCeti.genericFiberTowerNatIso (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] :
              CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R L))) ≅ (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))).comp (CategoryTheory.Over.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L))))

              Direct scalar extension from R to L is naturally isomorphic to scalar extension first to K and then to L.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem TauCeti.isPullback_genericFiberTower (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
                CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp (genericFiberι K L (genericFiber R K toBase).hom) (genericFiberι R K toBase)) (genericFiber K L (genericFiber R K toBase).hom).hom toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R L)))

                Iterated scalar extension from R through K to L is a pullback of the direct map from R to L.

                source
                noncomputable def TauCeti.genericFiberTowerIso (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
                (genericFiber K L (genericFiber R K toBase).hom).left ≅ (genericFiber R L toBase).left

                Iterated scalar extension is canonically isomorphic to direct scalar extension.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem TauCeti.genericFiberTowerIso_hom_genericFiberι (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
                  CategoryTheory.CategoryStruct.comp (genericFiberTowerIso R K L toBase).hom (genericFiberι R L toBase) = CategoryTheory.CategoryStruct.comp (genericFiberι K L (genericFiber R K toBase).hom) (genericFiberι R K toBase)

                  The scalar-extension tower isomorphism commutes with the projections to the total space.

                  source
                  @[simp]
                  theorem TauCeti.genericFiberTowerIso_hom_genericFiberι_assoc (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) :
                  CategoryTheory.CategoryStruct.comp (genericFiberTowerIso R K L toBase).hom (CategoryTheory.CategoryStruct.comp (genericFiberι R L toBase) h) = CategoryTheory.CategoryStruct.comp (genericFiberι K L (genericFiber R K toBase).hom) (CategoryTheory.CategoryStruct.comp (genericFiberι R K toBase) h)

                  The scalar-extension tower isomorphism commutes with the projections to the total space.

                  source
                  @[simp]
                  theorem TauCeti.genericFiberTowerIso_hom_hom (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
                  CategoryTheory.CategoryStruct.comp (genericFiberTowerIso R K L toBase).hom (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R L)))) = (genericFiber K L (genericFiber R K toBase).hom).hom

                  The scalar-extension tower isomorphism commutes with the projections to Spec L.

                  source
                  @[simp]
                  theorem TauCeti.genericFiberTowerIso_hom_hom_assoc (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧L ⟶ Z) :
                  CategoryTheory.CategoryStruct.comp (genericFiberTowerIso R K L toBase).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R L)))) h) = CategoryTheory.CategoryStruct.comp (genericFiber K L (genericFiber R K toBase).hom).hom h

                  The scalar-extension tower isomorphism commutes with the projections to Spec L.

                  source
                  @[simp]
                  theorem TauCeti.genericFiberTowerIso_inv_genericFiberι (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
                  CategoryTheory.CategoryStruct.comp (genericFiberTowerIso R K L toBase).inv (CategoryTheory.CategoryStruct.comp (genericFiberι K L (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))))) (genericFiberι R K toBase)) = genericFiberι R L toBase

                  The inverse scalar-extension tower isomorphism commutes with the projections to the total space.

                  source
                  @[simp]
                  theorem TauCeti.genericFiberTowerIso_inv_genericFiberι_assoc (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) :
                  CategoryTheory.CategoryStruct.comp (genericFiberTowerIso R K L toBase).inv (CategoryTheory.CategoryStruct.comp (genericFiberι K L (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))))) (CategoryTheory.CategoryStruct.comp (genericFiberι R K toBase) h)) = CategoryTheory.CategoryStruct.comp (genericFiberι R L toBase) h

                  The inverse scalar-extension tower isomorphism commutes with the projections to the total space.

                  source
                  @[simp]
                  theorem TauCeti.genericFiberTowerIso_inv_hom (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) :
                  CategoryTheory.CategoryStruct.comp (genericFiberTowerIso R K L toBase).inv (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))) = (genericFiber R L toBase).hom

                  The inverse scalar-extension tower isomorphism commutes with the projections to Spec L.

                  source
                  @[simp]
                  theorem TauCeti.genericFiberTowerIso_inv_hom_assoc (R K L : Type u) [CommRing R] [CommRing K] [CommRing L] [Algebra R K] [Algebra K L] [Algebra R L] [IsScalarTower R K L] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧L ⟶ Z) :
                  CategoryTheory.CategoryStruct.comp (genericFiberTowerIso R K L toBase).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))) h) = CategoryTheory.CategoryStruct.comp (genericFiber R L toBase).hom h

                  The inverse scalar-extension tower isomorphism commutes with the projections to Spec L.