Module

GradedSubalgebra.lean

Nyll.SchemeTheory.RingTheory.Descent.GradedSubalgebra

16 declarations indexed from sourceView source ↗

Module documentation

Descent of a grading to a homogeneous subalgebra

The grading is the inverse image of the upstairs homogeneous pieces. Its direct-sum retractions compare scalar extension degree by degree; this is a concrete construction, independent of how the subalgebra was obtained.

Imports5

Mathlib.RingTheory.GradedAlgebra.Basic
Mathlib.RingTheory.IsTensorProduct
Mathlib.RingTheory.TensorProduct.Basic
Mathlib.Tactic.SplitIfs
Nyll.SchemeTheory.RingTheory.HomogeneousIdealMap

Imported by1

Nyll.SchemeTheory.RingTheory.Descent.All

def

𝒜

L42 ↗

SchemeTheory.GradedSubalgebra.𝒜

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')

Lean source · statement

def 𝒜 (n : ℕ) : Submodule S A

theorem

mem_𝒜

L45 ↗

SchemeTheory.GradedSubalgebra.mem_𝒜

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
omit [GradedAlgebra 𝒜'] in

Lean source · statement

theorem mem_𝒜 {n : ℕ} {a : A} : a ∈ 𝒜 S' A' 𝒜' A n ↔ (a : A') ∈ 𝒜' n

instance

gradedMonoid

L47 ↗

SchemeTheory.GradedSubalgebra.gradedMonoid

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')

Lean source · full declaration

instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb

theorem

isInternal

L57 ↗

SchemeTheory.GradedSubalgebra.isInternal

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
include hhom in

Lean source · statement

theorem isInternal : DirectSum.IsInternal (𝒜 S' A' 𝒜' A)

def

gradedAlgebra

L114 ↗

SchemeTheory.GradedSubalgebra.gradedAlgebra

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)

Lean source · statement

def gradedAlgebra : GradedAlgebra (𝒜 S' A' 𝒜' A)

theorem

coe_decompose

L117 ↗

SchemeTheory.GradedSubalgebra.coe_decompose

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)

Lean source · full declaration

theorem coe_decompose (a : A) (n : ℕ) :
    let := gradedAlgebra S' A' 𝒜' A hhom
    (((DirectSum.decompose (𝒜 S' A' 𝒜' A) a n : A) : A') =
      (DirectSum.decompose 𝒜' (a : A') n : A')) := by
  intro inst
  classical
  have h := DirectSum.sum_support_decompose (𝒜 S' A' 𝒜' A) a
  have h' : (a : A') = ∑ i ∈ (DirectSum.decompose (𝒜 S' A' 𝒜' A) a).support,
      (((DirectSum.decompose (𝒜 S' A' 𝒜' A) a i : A) : A')) := by
    rw [← AddSubmonoidClass.coe_finsetSum]
    exact congrArg Subtype.val h.symm
  conv_rhs => rw [← GradedAlgebra.proj_apply, h', map_sum]
  have key : ∀ i, GradedAlgebra.proj 𝒜' n (((DirectSum.decompose (𝒜 S' A' 𝒜' A) a i : A) : A')) =
      if i = n then (((DirectSum.decompose (𝒜 S' A' 𝒜' A) a i : A) : A')) else 0 := by
    intro i
    rw [GradedAlgebra.proj_apply]
    have hmem : (((DirectSum.decompose (𝒜 S' A' 𝒜' A) a i : A) : A')) ∈ 𝒜' i :=
      (DirectSum.decompose (𝒜 S' A' 𝒜' A) a i).2
    split_ifs with hi
    · subst hi; exact DirectSum.decompose_of_mem_same 𝒜' hmem
    · exact DirectSum.decompose_of_mem_ne 𝒜' hmem hi
  simp_rw [key]
  rw [Finset.sum_ite_eq']
  split_ifs with hn
  · rfl
  · rw [DFinsupp.notMem_support_iff.mp hn]; rfl

theorem

h𝒜

L147 ↗

SchemeTheory.GradedSubalgebra.h𝒜

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
section BaseChange
omit [GradedAlgebra 𝒜'] in

Lean source · statement

theorem h𝒜 (n : ℕ) : ∀ a ∈ 𝒜 S' A' 𝒜' A n, A.val a ∈ 𝒜' n

abbrev

valn

L149 ↗

SchemeTheory.GradedSubalgebra.valn

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
section BaseChange

Lean source · statement

abbrev valn (n : ℕ) : 𝒜 S' A' 𝒜' A n →ₗ[S] (𝒜' n).restrictScalars S

abbrev

G

L152 ↗

SchemeTheory.GradedSubalgebra.G

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
section BaseChange

Lean source · statement

abbrev G : S' ⊗[S] A →ₐ[S] A'

theorem

G_tmul

L155 ↗

SchemeTheory.GradedSubalgebra.G_tmul

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
section BaseChange

Lean source · statement

theorem G_tmul (s : S') (a : A) : G S' A' A (s ⊗ₜ[S] a) = s • (a : A')

abbrev

gn

L158 ↗

SchemeTheory.GradedSubalgebra.gn

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
section BaseChange

Lean source · statement

abbrev gn (n : ℕ) :
    S' ⊗[S] ↥(𝒜 S' A' 𝒜' A n) →ₗ[S'] ↥((𝒜' n).restrictScalars S)

theorem

coe_gn

L163 ↗

SchemeTheory.GradedSubalgebra.coe_gn

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
section BaseChange
omit [GradedAlgebra 𝒜'] in

Lean source · statement

theorem coe_gn (n : ℕ) (z : S' ⊗[S] ↥(𝒜 S' A' 𝒜' A n)) :
    ((gn S' A' 𝒜' A n z : ↥((𝒜' n).restrictScalars S)) : A') =
      G S' A' A (LinearMap.lTensor S' (𝒜 S' A' 𝒜' A n).subtype z)

theorem

exists_retraction

L174 ↗

SchemeTheory.GradedSubalgebra.exists_retraction

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
section BaseChange
include hhom in

Lean source · statement

theorem exists_retraction (n : ℕ) :
    ∃ r : A →ₗ[S] ↥(𝒜 S' A' 𝒜' A n), (∀ x : ↥(𝒜 S' A' 𝒜' A n), r x = x) ∧
      ∀ a : A, ((r a : A) : A') = (DirectSum.decompose 𝒜' (a : A') n : A')

theorem

bijective_gn

L190 ↗

SchemeTheory.GradedSubalgebra.bijective_gn

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
section BaseChange
include hhom in

Lean source · statement

theorem bijective_gn (hbij : Function.Bijective (G S' A' A)) (n : ℕ) :
    Function.Bijective (gn S' A' 𝒜' A n)

theorem

isBaseChange

L225 ↗

SchemeTheory.GradedSubalgebra.isBaseChange

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
namespace SchemeTheory.GradedSubalgebra
variable {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
  (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
  (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
  (A : Subalgebra S A')
local instance gradedMonoid : SetLike.GradedMonoid (𝒜 S' A' 𝒜' A) where
  one_mem := by rw [mem_𝒜]; exact SetLike.one_mem_graded 𝒜'
  mul_mem := fun i j a b ha hb => by
    rw [mem_𝒜] at ha hb ⊢
    rw [Subalgebra.coe_mul]
    exact SetLike.mul_mem_graded ha hb
variable (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A)
section BaseChange
include hhom in

Lean source · statement

theorem isBaseChange (hbij : Function.Bijective (G S' A' A)) (n : ℕ) :
    IsBaseChange S' (valn S' A' 𝒜' A n)

theorem

exists_gradedAlgebra_isBaseChange_of_bijective_of_decompose_mem

L239 ↗

Subalgebra.exists_gradedAlgebra_isBaseChange_of_bijective_of_decompose_mem

Documentation

A subalgebra closed under homogeneous components inherits a grading. If scalar extension recovers the full algebra, each degree is also obtained by base change.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open TensorProduct DirectSum
universe u
open SchemeTheory.GradedSubalgebra in

Lean source · full declaration

theorem Subalgebra.exists_gradedAlgebra_isBaseChange_of_bijective_of_decompose_mem
    {S : Type u} [CommRing S] (S' : Type u) [CommRing S'] [Algebra S S']
    (A' : Type u) [CommRing A'] [Algebra S A'] [Algebra S' A'] [IsScalarTower S S' A']
    (𝒜' : ℕ → Submodule S' A') [GradedAlgebra 𝒜']
    (A : Subalgebra S A')
    (hbij : Function.Bijective
      (Algebra.TensorProduct.lift (IsScalarTower.toAlgHom S S' A') A.val
        (fun _ _ => Commute.all _ _)))
    (hhom : ∀ a ∈ A, ∀ n : ℕ, (DirectSum.decompose 𝒜' a n : A') ∈ A) :
    ∃ (𝒜 : ℕ → Submodule S A) (_ : GradedAlgebra 𝒜) (h𝒜 : ∀ n, ∀ a ∈ 𝒜 n, A.val a ∈ 𝒜' n),
      (∀ (n : ℕ) (a : A), (a : A') ∈ 𝒜' n → a ∈ 𝒜 n) ∧
      (∀ n, IsBaseChange S' ((A.val.toLinearMap.restrict (p := 𝒜 n)
        (q := (𝒜' n).restrictScalars S) (h𝒜 n))
        : 𝒜 n →ₗ[S] (𝒜' n).restrictScalars S)) ∧
      HomogeneousIdeal.irrelevant 𝒜' ≤
        (HomogeneousIdeal.irrelevant 𝒜).map
          ({ A.val.toRingHom with map_mem := fun h => h𝒜 _ _ h } : 𝒜 →+*ᵍ 𝒜') := by
  classical
  refine ⟨SchemeTheory.GradedSubalgebra.𝒜 S' A' 𝒜' A, gradedAlgebra S' A' 𝒜' A hhom,
    SchemeTheory.GradedSubalgebra.h𝒜 S' A' 𝒜' A, fun n a ha => ha,
    fun n => isBaseChange S' A' 𝒜' A hhom hbij n, ?_⟩
  let := gradedAlgebra S' A' 𝒜' A hhom
  apply HomogeneousIdeal.irrelevant_le_map_of_forall_le_span_image
  intro n _ x hx
  let x' : (𝒜' n).restrictScalars S := ⟨x, hx⟩
  have hspan : ∀ y : (𝒜' n).restrictScalars S,
      (y : A') ∈ Submodule.span S'
        (A.val.toRingHom '' (SchemeTheory.GradedSubalgebra.𝒜 S' A' 𝒜' A n : Set A)) := by
    intro y
    induction y using (isBaseChange S' A' 𝒜' A hhom hbij n).inductionOn with
    | tmul m => exact Submodule.subset_span ⟨m, m.2, rfl⟩
    | smul t y hy => exact Submodule.smul_mem _ t hy
    | add y z hy hz => exact Submodule.add_mem _ hy hz
  exact hspan x'

Module documentation

Descent of a grading to a homogeneous subalgebra

Declarations