OAI/Algebra/GroupRing/TypedComponent.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TorsionFreeZeroDivisors.TypedComponent.graph line 13
2. abbrev OAI.TorsionFreeZeroDivisors.TypedComponent.Vertex line 14
3. def OAI.TorsionFreeZeroDivisors.TypedComponent.out line 15
4. abbrev OAI.TorsionFreeZeroDivisors.TypedComponent.Dart line 16
5. def OAI.TorsionFreeZeroDivisors.TypedComponent.lift line 17
6. lemma OAI.TorsionFreeZeroDivisors.TypedComponent.lift_injective line 19
7. def OAI.TorsionFreeZeroDivisors.TypedComponent.reverse line 27
8. lemma OAI.TorsionFreeZeroDivisors.TypedComponent.lift_reverse line 31
9. lemma OAI.TorsionFreeZeroDivisors.TypedComponent.reverse_reverse line 33
10. lemma OAI.TorsionFreeZeroDivisors.TypedComponent.label_reverse line 37
11. def OAI.TorsionFreeZeroDivisors.TypedComponent.base line 40
12. abbrev OAI.TorsionFreeZeroDivisors.ComponentFactors.CA line 48
13. abbrev OAI.TorsionFreeZeroDivisors.ComponentFactors.CB line 49
14. theorem OAI.TorsionFreeZeroDivisors.ComponentFactors.product_zero line 52

    Source documentation

    Actual full components in the chosen sample, with every outgoing edge retained. Parallel simultaneous steps cancel as distinct signed flags.

    theorem product_zero (letter : Types.Letter→G) (g : CA rep r x→G) (h : CB rep r y→G)
        (hg : ∀ d : TypedComponent.Dart (@Types.outgoingA rep) r.1 x,
          g (TypedComponent.reverse _ r.1 x d).val.1=g d.val.1*letter d.val.2)
        (hh : ∀ d : TypedComponent.Dart (@Types.outgoingB rep) r.2 y,
          h (TypedComponent.reverse _ r.2 y d).val.1=h d.val.1*letter d.val.2) :
        (∑ a,MonoidAlgebra.single (g a) (1 : ZMod 2)) *
          (∑ b,MonoidAlgebra.single ((h b)⁻¹) (1 : ZMod 2))=0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.ComponentFactors.CA, OAI.TorsionFreeZeroDivisors.ComponentFactors.CB, OAI.TorsionFreeZeroDivisors.TypedComponent.Dart, OAI.TorsionFreeZeroDivisors.Types.outgoingA, OAI.TorsionFreeZeroDivisors.TypedComponent.reverse, OAI.TorsionFreeZeroDivisors.Types.outgoingB

15. theorem OAI.TorsionFreeZeroDivisors.ComponentFactors.nonzero_factors line 71

    Source documentation

    Given the source's root nontriviality endpoint, these very sums are the nonzero factors. No pairwise distinctness of the other vertex labels is used.

    theorem nonzero_factors
        (letter : Types.Letter→G) (g : CA rep r x→G) (h : CB rep r y→G)
        (hg : ∀ d : TypedComponent.Dart (@Types.outgoingA rep) r.1 x,
          g (TypedComponent.reverse _ r.1 x d).val.1=g d.val.1*letter d.val.2)
        (hh : ∀ d : TypedComponent.Dart (@Types.outgoingB rep) r.2 y,
          h (TypedComponent.reverse _ r.2 y d).val.1=h d.val.1*letter d.val.2)
        (hx : g (TypedComponent.base _ r.1 x)=1) (hy : h (TypedComponent.base _ r.2 y)=1)
        (hux : ∀ a,g a=1 → a=TypedComponent.base _ r.1 x)
        (huy : ∀ b,h b=1 → b=TypedComponent.base _ r.2 y) :
        ∃ α β : MonoidAlgebra (ZMod 2) G,α≠0 ∧ β≠0 ∧ α*β=0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.ComponentFactors.CA, OAI.TorsionFreeZeroDivisors.ComponentFactors.CB, OAI.TorsionFreeZeroDivisors.TypedComponent.Dart, OAI.TorsionFreeZeroDivisors.Types.outgoingA, OAI.TorsionFreeZeroDivisors.TypedComponent.reverse, OAI.TorsionFreeZeroDivisors.Types.outgoingB, OAI.TorsionFreeZeroDivisors.TypedComponent.base

16. def OAI.TorsionFreeZeroDivisors.ConcreteFactors.leftValue line 93
17. def OAI.TorsionFreeZeroDivisors.ConcreteFactors.rightValue line 95
18. lemma OAI.TorsionFreeZeroDivisors.ConcreteFactors.left_edge line 97
19. lemma OAI.TorsionFreeZeroDivisors.ConcreteFactors.right_edge line 106
20. lemma OAI.TorsionFreeZeroDivisors.ConcreteFactors.left_root line 115
21. lemma OAI.TorsionFreeZeroDivisors.ConcreteFactors.right_root line 117
22. def OAI.TorsionFreeZeroDivisors.ConcreteFactors.alpha line 119
23. def OAI.TorsionFreeZeroDivisors.ConcreteFactors.beta line 121
24. theorem OAI.TorsionFreeZeroDivisors.ConcreteFactors.product_zero line 125

    Source documentation

    The author's factors multiply to zero in the exact finite graph presentation, for every matching sample. Nonvanishing is a separate geometric obligation.

    theorem product_zero : alpha rep r x*beta rep r y=0 :=
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConcreteFactors.alpha, OAI.TorsionFreeZeroDivisors.ConcreteFactors.beta

25. lemma OAI.TorsionFreeZeroDivisors.ConcreteFactors.alpha_nonzero line 128
26. lemma OAI.TorsionFreeZeroDivisors.ConcreteFactors.beta_nonzero line 132
27. def OAI.TorsionFreeZeroDivisors.SumPort.leftHom line 145
28. def OAI.TorsionFreeZeroDivisors.SumPort.rightHom line 150
29. theorem OAI.TorsionFreeZeroDivisors.ConcreteFactors.alpha_nonzero_of_separator line 171

    Source documentation

    Source disk nontriviality suffices for the literal left factor, without assuming distinctness of the other vertex values. The sharp separator is the explicit still-unclosed premise, not an axiom or a claim of the main theorem.

    theorem alpha_nonzero_of_separator : alpha rep r x≠0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConcreteFactors.alpha

30. theorem OAI.TorsionFreeZeroDivisors.ConcreteFactors.beta_nonzero_of_separator line 186

    Source documentation

    The right factor's identity coefficient is likewise exactly one; its inversion does not require a global component embedding theorem.

    theorem beta_nonzero_of_separator : beta rep r y≠0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConcreteFactors.beta

31. theorem OAI.TorsionFreeZeroDivisors.ConcreteFactors.both_nonzero line 211

    Source documentation

    Both original factors are now unconditionally nonzero for the sampled no-arrangement graphs. The literal sharp separator is proved, not assumed.

    theorem both_nonzero : alpha rep r x≠0 ∧ beta rep r y≠0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConcreteFactors.alpha, OAI.TorsionFreeZeroDivisors.ConcreteFactors.beta

32. theorem OAI.TorsionFreeZeroDivisors.SampleGraph.exists_nonzero_factors line 223

    Source documentation

    An actual sample with both nonzero factors in its exact finitely presented group. Torsion-freeness and the topological classifying-space clause are NOT asserted here; they remain obligations for the main theorem.

    theorem exists_nonzero_factors :
        ∃ (rep : ℕ) (r : ActualPatternEvent.Match rep) (x : VA rep) (y : VB rep),
          r∈ActualPatternEvent.samples rep ∧ 2≤L (size rep) ∧
          GraphSample.Diameters rep r ∧
          IsEmpty (BoundedSystem (PlanarParameters.C PathSystem.ε ClosedWords.D)
            (PlanarParameters.K PathSystem.ε ClosedWords.D)
            (PlanarParameters.sides PathSystem.ε ClosedWords.D) rep r x y) ∧
          ConcreteFactors.alpha rep r x≠0 ∧ ConcreteFactors.beta rep r y≠0 ∧
          ConcreteFactors.alpha rep r x*ConcreteFactors.beta rep r y=0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ActualPatternEvent.Match, OAI.TorsionFreeZeroDivisors.SampleGraph.VA, OAI.TorsionFreeZeroDivisors.SampleGraph.VB, OAI.TorsionFreeZeroDivisors.ActualPatternEvent.samples, OAI.TorsionFreeZeroDivisors.GraphSample.Diameters, OAI.TorsionFreeZeroDivisors.SampleGraph.BoundedSystem, OAI.TorsionFreeZeroDivisors.PlanarParameters.C, OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.ε, OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.D, OAI.TorsionFreeZeroDivisors.PlanarParameters.K, OAI.TorsionFreeZeroDivisors.PlanarParameters.sides, OAI.TorsionFreeZeroDivisors.ConcreteFactors.alpha, OAI.TorsionFreeZeroDivisors.ConcreteFactors.beta

33. theorem OAI.TorsionFreeZeroDivisors.finitely_presented_zero_divisors line 249

    Source documentation

    Complete algebraic zero-divisor part of the construction, without the still-missing ordinary torsion-free and finite K(G,1) conclusions.

    theorem finitely_presented_zero_divisors :
        ∃ (G : Type) (inst : Group G), letI : Group G := inst
    …