Code

CommAlgebras as CommRingHoms#1145

Code

Draft

felixwellen wants to merge 83 commits intomasteragda/cubical:masterfrom fwellen/ring_with_hom_algebrasagda/cubical:fwellen/ring_with_hom_algebrasCopy head branch name to clipboard

+4,425-2,005

Commits

Commits on Sep 30, 2024

• move univalence code

  felixwellen

  committed
  d464874

  Copy full SHA for d464874

• start...

  felixwellen

  committed
  9054103

  Copy full SHA for 9054103

• boilerplate

  felixwellen

  committed
  6bd6176

  Copy full SHA for 6bd6176

• fix auto-univalence

  felixwellen

  committed
  acde70a

  Copy full SHA for acde70a

• fix FreeCommAlg

  felixwellen

  committed
  2d9b18f

  Copy full SHA for 2d9b18f

• fix subalgebra

  felixwellen

  committed
  16ba911

  Copy full SHA for 16ba911

• fix FPAlgebra

  felixwellen

  committed
  b1bac5c

  Copy full SHA for b1bac5c

• copy Evans approach for Groups

  felixwellen

  committed
  487fe8d

  Copy full SHA for 487fe8d

• refactor

  felixwellen

  committed
  a33924c

  Copy full SHA for a33924c

• refactor

  felixwellen

  committed
  ef58e50

  Copy full SHA for ef58e50

• no-eta for algebra structures

  felixwellen

  committed
  90bbfac

  Copy full SHA for 90bbfac

• opaque quotients, fix unicity

  felixwellen

  committed
  83e9919

  Copy full SHA for 83e9919

• fast tc for quotient comm rings

  felixwellen

  committed
  bbda88b

  Copy full SHA for bbda88b

• uniform indentation

  felixwellen

  committed
  35274b5

  Copy full SHA for 35274b5

• cleanup /remove flag

  felixwellen

  committed
  41bc2a3

  Copy full SHA for 41bc2a3

• improve names

  felixwellen

  committed
  a498039

  Copy full SHA for a498039

• clean up

  felixwellen

  committed
  3e57fdd

  Copy full SHA for 3e57fdd

• WIP: deactivate problematic code

  felixwellen

  committed
  79f932c

  Copy full SHA for 79f932c

• refactor/simplify

  felixwellen

  committed
  34fc5c9

  Copy full SHA for 34fc5c9

• WIP

  felixwellen

  committed
  76f8c22

  Copy full SHA for 76f8c22

• start with stuff on the new comm alg

  felixwellen

  committed
  8a0c069

  Copy full SHA for 8a0c069

• Revert "Auxiliary commit to revert individual files from c5e74aa"

  Show description for 5801fd3
  felixwellen

  committed
  5801fd3

  Copy full SHA for 5801fd3

• Quotients

  felixwellen

  committed
  2725661

  Copy full SHA for 2725661

• update comm ring hom interface

  felixwellen

  committed
  9b9e0ac

  Copy full SHA for 9b9e0ac

• more boilerplate

  felixwellen

  committed
  b83bf0f

  Copy full SHA for b83bf0f

• kernels

  felixwellen

  committed
  a07d7d7

  Copy full SHA for a07d7d7

• syntax for new algebras

  felixwellen

  committed
  bd52821

  Copy full SHA for bd52821

• more on comm ring quotients

  felixwellen

  committed
  3a9a310

  Copy full SHA for 3a9a310

• fix

  felixwellen

  committed
  4a9842f

  Copy full SHA for 4a9842f

• algebra quotients

  felixwellen

  committed
  f1433a8

  Copy full SHA for f1433a8

• more opaque definitions, more use of set-level equalities

  felixwellen

  committed
  d8b07b4

  Copy full SHA for d8b07b4

• commRingHom fixes

  felixwellen

  committed
  55d58c6

  Copy full SHA for 55d58c6

• unit comm algebra

  felixwellen

  committed
  4bacbaa

  Copy full SHA for 4bacbaa

• quotients

  felixwellen

  committed
  194e456

  Copy full SHA for 194e456

• no-eta for the equations of a ring

  felixwellen

  committed
  62d9af2

  Copy full SHA for 62d9af2

• WIP: Univalence

  felixwellen

  committed
  b4475a4

  Copy full SHA for b4475a4

• equality characterization with help from Evan

  felixwellen

  committed
  24582d2

  Copy full SHA for 24582d2

• WIP

  felixwellen

  committed
  58d2e89

  Copy full SHA for 58d2e89

• typevariate polynomials as comm ring

  felixwellen

  committed
  78a6beb

  Copy full SHA for 78a6beb

• polynomials as comm algebra

  felixwellen

  committed
  bb224c5

  Copy full SHA for bb224c5

• remove opaque structure again

  Show description for 6667098
  felixwellen

  committed
  6667098

  Copy full SHA for 6667098

• Revert "WIP: deactivate problematic code"

  Show description for f13c4c1
  felixwellen

  committed
  f13c4c1

  Copy full SHA for f13c4c1

• make one example more meaningful

  felixwellen

  committed
  6052d37

  Copy full SHA for 6052d37

• univalence for comm algebras with Evans help

  felixwellen

  committed
  3079c8d

  Copy full SHA for 3079c8d

• various fixes, continue with typevariate polynomials

  felixwellen

  committed
  527861f

  Copy full SHA for 527861f

• induce a com ring hom

  felixwellen

  committed
  631e9bc

  Copy full SHA for 631e9bc

• Comm ring of polynomials on a general variable type and its universal property

  felixwellen

  committed
  2f43b22

  Copy full SHA for 2f43b22

• improve interface

  felixwellen

  committed
  57c7b16

  Copy full SHA for 57c7b16

• more interface, more opaque

  felixwellen

  committed
  b576f32

  Copy full SHA for b576f32

• fix

  felixwellen

  committed
  a19fbd5

  Copy full SHA for a19fbd5

• start with localization, fixes, more opaque things

  felixwellen

  committed
  5089c7f

  Copy full SHA for 5089c7f

• make ring quotients' isRing opaque instead of no-eta

  felixwellen

  committed
  e9f0616

  Copy full SHA for e9f0616

• update to new interface for comm ring homs

  felixwellen

  committed
  2de9d4f

  Copy full SHA for 2de9d4f

• update to new interface for comm ring homs

  felixwellen

  committed
  94770d3

  Copy full SHA for 94770d3

• stub for polynomials, fix

  felixwellen

  committed
  74d51ab

  Copy full SHA for 74d51ab

• finish localization

  felixwellen

  committed
  3573a4c

  Copy full SHA for 3573a4c

• start with OnCoproduct, change default notation for R[I]

  felixwellen

  committed
  414b2f2

  Copy full SHA for 414b2f2

• universal property of polynomials as rings

  felixwellen

  committed
  0b76ab7

  Copy full SHA for 0b76ab7

• move old CommAlgebra

  felixwellen

  committed
  1c71ebd

  Copy full SHA for 1c71ebd

• category structure

  felixwellen

  committed
  33c060b

  Copy full SHA for 33c060b

• fix ref

  felixwellen

  committed
  5ec0ba4

  Copy full SHA for 5ec0ba4

• fix/move algebra as module

  felixwellen

  committed
  acfd747

  Copy full SHA for acfd747

• refs

  felixwellen

  committed
  0f5053e

  Copy full SHA for 0f5053e

• remove old CommAlgebra.agda, move all refs

  felixwellen

  committed
  367e8bd

  Copy full SHA for 367e8bd

• fix

  felixwellen

  committed
  71d44b9

  Copy full SHA for 71d44b9

• make the new CommAlgebra the default

  felixwellen

  committed
  7cc50a6

  Copy full SHA for 7cc50a6

• remove no-eta for structure

  felixwellen

  committed
  f21b3a1

  Copy full SHA for f21b3a1

• start with fp algebras

  felixwellen

  committed
  703e717

  Copy full SHA for 703e717

• small additions

  felixwellen

  committed
  5384862

  Copy full SHA for 5384862

• WIP: start with FP algebra examples

  felixwellen

  committed
  6e12f6c

  Copy full SHA for 6e12f6c

• change def, fix thinghs

  felixwellen

  committed
  1f44a50

  Copy full SHA for 1f44a50

• fix localization, adapt univalence, rearrange base

  felixwellen

  committed
  a95079a

  Copy full SHA for a95079a

• fix quotients

  felixwellen

  committed
  4ba4d01

  Copy full SHA for 4ba4d01

• fix

  felixwellen

  committed
  b2f7072

  Copy full SHA for b2f7072

• fix

  felixwellen

  committed
  89ecaa2

  Copy full SHA for 89ecaa2

• solver examples with new comm algebras

  felixwellen

  committed
  7293a0d

  Copy full SHA for 7293a0d

• fix

  felixwellen

  committed
  bbd32fd

  Copy full SHA for bbd32fd

• more boilterplate, morphism contructor

  felixwellen

  committed
  9286b26

  Copy full SHA for 9286b26

• polynomial ring is fp

  felixwellen

  committed
  14c6d4c

  Copy full SHA for 14c6d4c

• add more calcualtions

  felixwellen

  committed
  ed48931

  Copy full SHA for ed48931

• port initial algebra

  felixwellen

  committed
  c6f62d4

  Copy full SHA for c6f62d4

Commits on Oct 1, 2024

• fix comment

  felixwellen

  committed
  bc7a252

  Copy full SHA for bc7a252

Commits on Oct 16, 2024

• WIP

  felixwellen

  committed
  7917b85

  Copy full SHA for 7917b85