Geometric orbit images of scheme actions

For a group object G acting on X in schemes over S, a section x gives an orbit morphism G ⟶ X. Its geometric orbit is the image of the underlying scheme map, including nonclosed points. Define its closure and boundary in the same underlying topological space. Translation by any section of G preserves all three sets, and moving the base section by the action gives the same orbit. The translation homeomorphisms assemble into an action of the sections of G on the underlying space of X, under which the orbit is invariant. Equivariant morphisms carry orbit images onto orbit images. Lifts of ambient translations through a monomorphism give automorphisms with the same group laws and preserve the induced base morphism.

No finite-type, smoothness, reducedness or connectedness assumption is needed. These statements supply the invariant sets on which local closedness and orbit-dimension arguments can be made with additional geometric hypotheses; no subscheme structure or comparison with rational-point orbits is asserted here.

The morphism identities come from TauCeti.orbitMap and TauCeti.translation, using Mathlib's native internal actions.

noncomputable def TauCeti.SchemeAction.orbit {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : Set ↥X.left

The full topological image of the orbit morphism of a section.

@[simp]

theorem TauCeti.SchemeAction.mem_orbit {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) (p : ↥X.left) : p ∈ orbit G x ↔ ∃ (g : ↥G.left), (CategoryTheory.Over.Hom.left (orbitMap G x)) g = p

A scheme point lies in the orbit precisely when it lifts along the orbit morphism.

theorem TauCeti.SchemeAction.orbit_def {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : orbit G x = Set.range ⇑(CategoryTheory.Over.Hom.left (orbitMap G x))

The geometric orbit is the full range of the orbit morphism.

noncomputable def TauCeti.SchemeAction.orbitClosure {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : Set ↥X.left

The closure of the full geometric orbit image.

noncomputable def TauCeti.SchemeAction.orbitBoundary {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : Set ↥X.left

The boundary of the orbit inside its closure.

theorem TauCeti.SchemeAction.orbitClosure_def {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : orbitClosure G x = closure (orbit G x)

Membership in the orbit closure is membership in the closure of the orbit image.

theorem TauCeti.SchemeAction.orbitBoundary_def {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : orbitBoundary G x = orbitClosure G x \ orbit G x

The orbit boundary is the orbit closure with the orbit removed.

@[simp]

theorem TauCeti.SchemeAction.mem_orbitBoundary {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) (p : ↥X.left) : p ∈ orbitBoundary G x ↔ p ∈ orbitClosure G x ∧ p ∉ orbit G x

Boundary membership consists of closure membership and failure of orbit membership.

theorem TauCeti.SchemeAction.orbit_subset_orbitClosure {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : orbit G x ⊆ orbitClosure G x

The geometric orbit is contained in its closure.

theorem TauCeti.SchemeAction.orbitBoundary_subset_orbitClosure {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : orbitBoundary G x ⊆ orbitClosure G x

The orbit boundary is contained in the orbit closure.

theorem TauCeti.SchemeAction.isClosed_orbitClosure {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : IsClosed (orbitClosure G x)

The orbit closure is closed.

theorem TauCeti.SchemeAction.isClosed_orbit_iff_orbitBoundary_eq_empty {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : IsClosed (orbit G x) ↔ orbitBoundary G x = ∅

The geometric orbit is closed exactly when its boundary is empty.

theorem TauCeti.SchemeAction.image_orbit {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X Y : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] [CategoryTheory.ModObj G Y] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) (f : X ⟶ Y) [CategoryTheory.IsModHom G f] : ⇑(CategoryTheory.Over.Hom.left f) '' orbit G x = orbit G (CategoryTheory.CategoryStruct.comp x f)

Equivariant morphisms carry geometric orbit images onto the corresponding orbit images.

theorem TauCeti.SchemeAction.orbitMap_left_translation {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (orbitMap G x)) (CategoryTheory.Over.Hom.left (translation X g).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (leftTranslation g).hom) (CategoryTheory.Over.Hom.left (orbitMap G x))

The underlying orbit morphism intertwines ambient translation with left translation.

theorem TauCeti.SchemeAction.orbitMap_left_translation_assoc {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) {Z : AlgebraicGeometry.Scheme} (h : X.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (orbitMap G x)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (translation X g).hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (leftTranslation g).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (orbitMap G x)) h)

The underlying orbit morphism intertwines ambient translation with left translation.

@[simp]

theorem TauCeti.SchemeAction.image_translation_orbit {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : ⇑(CategoryTheory.Over.Hom.left (translation X g).hom) '' orbit G x = orbit G x

Translation by a group section preserves the full orbit image.

@[simp]

theorem TauCeti.SchemeAction.image_translation_orbitClosure {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : ⇑(CategoryTheory.Over.Hom.left (translation X g).hom) '' orbitClosure G x = orbitClosure G x

Translation preserves the closure, including any nonclosed scheme points.

@[simp]

theorem TauCeti.SchemeAction.image_translation_orbitBoundary {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : ⇑(CategoryTheory.Over.Hom.left (translation X g).hom) '' orbitBoundary G x = orbitBoundary G x

Translation preserves the orbit boundary as a set of all scheme points.

@[simp]

theorem TauCeti.SchemeAction.orbit_smul {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : orbit G (g • x) = orbit G x

Moving the base section by a group section leaves its geometric orbit unchanged.

@[instance_reducible]

noncomputable def TauCeti.SchemeAction.translationMulAction {S : AlgebraicGeometry.Scheme} (G X : CategoryTheory.Over S) [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] : MulAction (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) ↥X.left

The global points of a group scheme act on the underlying space of a scheme it acts on, each acting through its translation automorphism. Install it locally to select this action.

theorem TauCeti.SchemeAction.translationMulAction_smul {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) (p : ↥X.left) : g • p = (CategoryTheory.Over.Hom.left (translation X g).hom) p

A global point acts through its translation automorphism.

theorem TauCeti.SchemeAction.translationMulAction_smul_apply {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) (y : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) (a : ↥(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S)).left) : g • (CategoryTheory.Over.Hom.left y) a = (CategoryTheory.Over.Hom.left (g • y)) a

On the point underlying a section, the translation action is the action on sections.

theorem TauCeti.SchemeAction.continuousConstSMul_translationMulAction {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] : ContinuousConstSMul (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) ↥X.left

Every global point acts by a homeomorphism.

theorem TauCeti.SchemeAction.preimage_smul_orbit {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : (fun (p : ↥X.left) => g • p) ⁻¹' orbit G x = orbit G x

Translation by a global point preserves the orbit, so the orbit is invariant under the translation action.

noncomputable def TauCeti.SchemeAction.liftTranslation {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : Y ≅ Y

Lifts of all ambient translations through a monomorphism are automorphisms. The inverse is the lift of translation by the inverse group section.

theorem TauCeti.SchemeAction.liftTranslation_hom {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : (liftTranslation i t ht g).hom = t g

The automorphism uses the prescribed lift as its forward morphism.

theorem TauCeti.SchemeAction.liftTranslation_inv {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : (liftTranslation i t ht g).inv = t g⁻¹

The inverse automorphism uses the lift of the inverse group section.

@[simp]

theorem TauCeti.SchemeAction.liftTranslation_hom_ι {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : CategoryTheory.CategoryStruct.comp (liftTranslation i t ht g).hom i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)

The lifted translation intertwines the monomorphism with ambient translation.

@[simp]

theorem TauCeti.SchemeAction.liftTranslation_hom_ι_assoc {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) {Z : AlgebraicGeometry.Scheme} (h : X.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftTranslation i t ht g).hom (CategoryTheory.CategoryStruct.comp i h) = CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (translation X g).hom) h)

The lifted translation intertwines the monomorphism with ambient translation.

@[simp]

theorem TauCeti.SchemeAction.liftTranslation_one {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) : liftTranslation i t ht 1 = CategoryTheory.Iso.refl Y

Translation by the identity lifts to the identity.

@[simp]

theorem TauCeti.SchemeAction.liftTranslation_mul {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g h : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : liftTranslation i t ht (g * h) = liftTranslation i t ht h ≪≫ liftTranslation i t ht g

Lifted translations compose in action order.

@[simp]

theorem TauCeti.SchemeAction.liftTranslation_inv_eq_symm {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : liftTranslation i t ht g⁻¹ = (liftTranslation i t ht g).symm

Inverse group sections lift to inverse automorphisms.

@[simp]

theorem TauCeti.SchemeAction.liftTranslation_inv_ι {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : CategoryTheory.CategoryStruct.comp (liftTranslation i t ht g).inv i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).inv)

The inverse lifted translation also intertwines the monomorphism.

@[simp]

theorem TauCeti.SchemeAction.liftTranslation_inv_ι_assoc {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) {Z : AlgebraicGeometry.Scheme} (h : X.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftTranslation i t ht g).inv (CategoryTheory.CategoryStruct.comp i h) = CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (translation X g).inv) h)

The inverse lifted translation also intertwines the monomorphism.

theorem TauCeti.SchemeAction.liftTranslation_hom_toBase {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : CategoryTheory.CategoryStruct.comp (liftTranslation i t ht g).hom (CategoryTheory.CategoryStruct.comp i X.hom) = CategoryTheory.CategoryStruct.comp i X.hom

Lifted translations preserve the structure morphism induced by the monomorphism.

theorem TauCeti.SchemeAction.liftTranslation_hom_toBase_assoc {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftTranslation i t ht g).hom (CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp X.hom h)) = CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp X.hom h)

Lifted translations preserve the structure morphism induced by the monomorphism.

theorem TauCeti.SchemeAction.liftTranslation_inv_toBase {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : CategoryTheory.CategoryStruct.comp (liftTranslation i t ht g).inv (CategoryTheory.CategoryStruct.comp i X.hom) = CategoryTheory.CategoryStruct.comp i X.hom

Inverse lifted translations preserve the induced structure morphism.

theorem TauCeti.SchemeAction.liftTranslation_inv_toBase_assoc {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftTranslation i t ht g).inv (CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp X.hom h)) = CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp X.hom h)

Inverse lifted translations preserve the induced structure morphism.

theorem TauCeti.SchemeAction.comp_liftTranslation_hom {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) (p : G.left ⟶ Y) (hp : CategoryTheory.CategoryStruct.comp p i = CategoryTheory.Over.Hom.left (orbitMap G x)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) : CategoryTheory.CategoryStruct.comp p (liftTranslation i t ht g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (leftTranslation g).hom) p

Any factorization of the orbit morphism through the monomorphism is equivariant for the lifted translations.

theorem TauCeti.SchemeAction.comp_liftTranslation_hom_assoc {S : AlgebraicGeometry.Scheme} {G X : CategoryTheory.Over S} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [CategoryTheory.Mono i] (t : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) → (Y ⟶ Y)) (ht : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G), CategoryTheory.CategoryStruct.comp (t g) i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) (p : G.left ⟶ Y) (hp : CategoryTheory.CategoryStruct.comp p i = CategoryTheory.Over.Hom.left (orbitMap G x)) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ G) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (liftTranslation i t ht g).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (leftTranslation g).hom) (CategoryTheory.CategoryStruct.comp p h)

Any factorization of the orbit morphism through the monomorphism is equivariant for the lifted translations.