Grace/Cumulus/Algebra/Image.g17

Open in Workbench Download source

Imports

Adjoin · Cardinal.FiniteImage

Declarations

Source

1-- Surjective images preserve finite generation of algebras (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Image8import Adjoin9import Cardinal.FiniteImage1011def subringComap (g B T : Set) : Set := {x ∈ B | g(x) ∈ T}1213section Maps14variable (B plus z minus times unit C sum o inverse product e g : Set)15notation ring S := (B, plus, z, minus, times, unit)16notation ring U := (C, sum, o, inverse, product, e)17hypothesis source : IsCommRing(S)18hypothesis target : IsCommRing(U)19hypothesis hom : IsRingHom(g, S, U)2021theorem subringComap.subring (T : Set)22  requires subring : IsSubring(U, T)23  shows IsSubring(S, subringComap(g, B, T))24proof25  have ordinary := IsCommRing.ring with source26  have zeroIn := IsRing.zero_in_carrier with ordinary27  have multiplicative := IsRing.multiplicative with ordinary28  have oneIn := IsMonoid.unit_in_carrier with multiplicative29  have zeroMem := IsSubring.zero_closed with subring30  have oneMem := IsSubring.one_closed with subring31  have negClosed := IsSubring.neg_closed with subring32  have addClosed := IsSubring.add_closed with subring33  have mulClosed := IsSubring.mul_closed with subring34  have zeroValue := IsRingHom.zero with hom35  have oneValue := IsRingHom.one with hom36  have subset : subringComap(g, B, T) ⊆ B37    intros x hx38    have data := subringComap.membership.forward with hx39    exact data.left40  unfold IsSubring41  refine ⟨subset, ⟨?_, ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩⟩42  . apply subringComap.membership.backward at g, B, T, z43    rw zeroValue44    refine ⟨zeroIn, zeroMem⟩45  . apply subringComap.membership.backward at g, B, T, unit46    rw oneValue47    refine ⟨oneIn, oneMem⟩48    intros x hx49    obtain ⟨member, value⟩ := subringComap.membership.forward with hx50    have closed := IsRing.neg_closed with ordinary, member51    have mapped := IsRingHom.neg with hom, member52    have output := ClosedUnary.mem with negClosed, value53    apply subringComap.membership.backward54    rw mapped55    refine ⟨closed, output⟩56    intros x hx y hy57    obtain ⟨memberX, valueX⟩ := subringComap.membership.forward with hx58    obtain ⟨memberY, valueY⟩ := subringComap.membership.forward with hy59    have closed := IsRing.add_closed with ordinary, memberX, memberY60    have mapped := IsRingHom.add with hom, memberX, memberY61    have output := ClosedBinary.mem with addClosed, valueX, valueY62    apply subringComap.membership.backward63    rw mapped64    refine ⟨closed, output⟩65    intros x hx y hy66    obtain ⟨memberX, valueX⟩ := subringComap.membership.forward with hx67    obtain ⟨memberY, valueY⟩ := subringComap.membership.forward with hy68    have closed := IsRing.mul_closed with ordinary, memberX, memberY69    have mapped := IsRingHom.mul with hom, memberX, memberY70    have output := ClosedBinary.mem with mulClosed, valueX, valueY71    apply subringComap.membership.backward72    rw mapped73    refine ⟨closed, output⟩7475end Maps7677section Algebras78variable (A add zero neg mul one B plus z minus times unit C sum o inverse product e f g : Set)79notation ring R := (A, add, zero, neg, mul, one)80notation ring S := (B, plus, z, minus, times, unit)81notation ring U := (C, sum, o, inverse, product, e)82hypothesis coefficients : IsCommRing(R)83hypothesis source : IsCommRing(S)84hypothesis target : IsCommRing(U)85hypothesis coefficientMap : IsRingHom(f, R, S)86hypothesis hom : IsRingHom(g, S, U)8788theorem Subalgebra.comap (T : Set)89  requires subalgebra : Subalgebra(compose(g, f, A, B, C), R, U, T)90  shows Subalgebra(f, R, S, subringComap(g, B, T))91proof92  have functionF := IsRingHom.function with coefficientMap93  have functionG := IsRingHom.function with hom94  have composite := compose.function at g, f, A, B, C with *95  have structure := subalgebra96  have subring := subringComap.subring with source, target, hom, structure.left97  have included := structure.right98  have image : functionImage(f, A, B) ⊆ subringComap(g, B, T)99    intros b hb100    obtain ⟨memberB, a, ha, value⟩ := functionImage.membership.forward with hb101    have compositeValue := compose.apply at g, f, A, B, C, a with *102    have imageValue := functionImage.value at compose(g, f, A, B, C), A, C, a with *103    have member := included with compose(g, f, A, B, C)(a), imageValue104    apply subringComap.membership.backward105    constructor106    . exact memberB107    . rw [value, ← compositeValue]108      exact member109  unfold Subalgebra110  refine ⟨subring, image⟩111112theorem algebraAdjoin.map_into (G : Set)113  requires bounded : G ⊆ S114  shows algebraAdjoin(f, R, S, G) ⊆ subringComap(g, B, algebraAdjoin(compose(g, f, A, B, C), R, U, functionImage(g, G, C)))115proof116  have composite := IsRingHom.compose with coefficients, coefficientMap, hom117  have function := IsRingHom.function with hom118  have imageBound := functionImage.subset at g, G, C119  have generated := algebraAdjoin.subalgebra with coefficients, target, composite, imageBound120  have contains := algebraAdjoin.contains with coefficients, target, composite, imageBound121  have preimage := Subalgebra.comap with coefficients, source, target, coefficientMap, hom, generated122  have generators : G ⊆ subringComap(g, B, algebraAdjoin(compose(g, f, A, B, C), R, U, functionImage(g, G, C)))123    intros x hx124    have member := bounded with x, hx125    have value := FunctionBetween.apply_closed with function, member126    have image : g(x) ∈ functionImage(g, G, C)127      apply functionImage.membership.backward128      refine ⟨value, x, hx, ?_⟩129      rfl130    have generatedValue := contains with g(x), image131    exact subringComap.membership.backward with ⟨member, generatedValue⟩132  exact algebraAdjoin.least with coefficients, source, coefficientMap, preimage, generators133134theorem algebraAdjoin.surjective_image (G : Set)135  requires onto : SurjectiveBetween(g, B, C)136  requires bounded : G ⊆ S137  requires generates : algebraAdjoin(f, R, S, G) = S138  shows algebraAdjoin(compose(g, f, A, B, C), R, U, functionImage(g, G, C)) = U139proof140  have composite := IsRingHom.compose with coefficients, coefficientMap, hom141  have subset := algebraAdjoin.subset at A, add, zero, neg, mul, one, C, sum, o, inverse, product, e, compose(g, f, A, B, C), functionImage(g, G, C) with *142  have mapped := algebraAdjoin.map_into with coefficients, source, target, coefficientMap, hom, bounded143  rw generates at mapped144  have surjection := onto145  apply Subset.antisymmetric with subset146  intros y hy147  obtain ⟨x, hx, edge⟩ := surjection.right with y, hy148  have value := FunctionBetween.apply_value with surjection.left, hx, edge149  have member := mapped with x, hx150  have data := subringComap.membership.forward with member151  rw value at data152  exact data.right153154theorem FinitelyGeneratedAlgebra.surjective_image155  requires finiteGeneration : FinitelyGeneratedAlgebra(f, R, S)156  requires onto : SurjectiveBetween(g, B, C)157  shows FinitelyGeneratedAlgebra(compose(g, f, A, B, C), R, U)158proof159  obtain ⟨G, finite, bounded, generates⟩ := finiteGeneration160  have function := IsRingHom.function with hom161  have imageFinite := Finite.function_image with function, finite, bounded162  have imageBound := functionImage.subset at g, G, C163  have imageGenerates := algebraAdjoin.surjective_image with coefficients, source, target, coefficientMap, hom, onto, bounded, generates164  unfold FinitelyGeneratedAlgebra165  refine ⟨functionImage(g, G, C), imageFinite, imageBound, imageGenerates⟩166167end Algebras168section Quotients169variable (A add zero neg mul one B plus z minus times unit f J : Set)170notation ring R := (A, add, zero, neg, mul, one)171notation ring S := (B, plus, z, minus, times, unit)172notation ring Q := S ⧸ J173hypothesis coefficients : IsCommRing(R)174hypothesis source : IsCommRing(S)175hypothesis hom : IsRingHom(f, R, S)176hypothesis ideal : IsIdeal(S, J)177178theorem FinitelyGeneratedAlgebra.quotient179  requires finiteGeneration : FinitelyGeneratedAlgebra(f, R, S)180  shows FinitelyGeneratedAlgebra(compose(quotientProjection(B, idealRelation(B, plus, minus, J)), f, A, B, Q), R, Q)181proof182  have target := idealQuotient.comm_ring with *183  have projection := idealQuotient.projection_hom with *184  have equivalence := idealRelation.equivalence with *185  have onto := quotientProjection.surjective with *186  exact FinitelyGeneratedAlgebra.surjective_image with coefficients, source, target, hom, projection, finiteGeneration, onto187188end Quotients189